Abstract
Systems ought to behave reasonably even in circumstances that are not anticipated in their specifications. We propose a definition of robustness for liveness specifications which prescribes, for any number of environment assumptions that are violated, a minimal number of system guarantees that must still be fulfilled. This notion of robustness can be formulated and realized using a Generalized Reactivity formula. We present an algorithm for synthesizing robust systems from such formulas. For the important special case of Generalized Reactivity formulas of rank 1, our algorithm improves the complexity of [PPS06] for large specifications with a small number of assumptions and guarantees.
This work was supported by EU grants 217069 (COCONUT), 248613 (DIAMOND), 215543 (COMBEST), and the European Network of Excellence ArtistDesign.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arora, A.: Closure and convergence: A foundation of fault-tolerant computing. IEEE Transatcions of Software Engineering 19, 1015–1027 (1993)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
Bloem, R., Chatterjee, K., Henzinger, T., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)
Bloem, R., Greimel, K., Henzinger, T., Jobstmann, B.: Synthesizing robust systems. In: Proc. Formal Methods in Computer Aided Design (FMCAD), pp. 85–92 (2009)
Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: Proceedings of the Design, Automation and Test in Europe, pp. 1188–1193 (2007)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 153–167. Springer, Heidelberg (2007)
de Alfaro, L., Faella, M.: Accelerated algorithms for 3-color parity games with an application to timed games. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 108–120. Springer, Heidelberg (2007)
Dijkstra, E.W.: Cooperating sequential processes. In: Genuys (ed.) Programming Languages, pp. 43–112. Academic Press, London (1968)
Dijkstra, E.: Self-stabilizing systems in spite of distributed control. Communications of the ACM 17, 643–644 (1974)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. 32nd IEEE Symposium on Foundations of Computer Science, October 1991, pp. 368–377 (1991)
Ebnenasir, A., Kulkarni, S.S., Arora, A.: Ftsyn: a framework for automatic synthesis of fault-tolerance. Software Tools for Technology Transfer 10, 455–471 (2008)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of the First Annual Symposium of Logic in Computer Science, June 1986, pp. 267–278 (1986)
Fey, G., Drechsler, R.: A basis for formal robustness checking. In: ISQED, pp. 784–789 (2008)
Greimel, K., Bloem, R., Jobstmann, B., Vardi, M.: Open implication. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 361–372. Springer, Heidelberg (2008)
Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007)
Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Kulkarni, S.S., Ebnnenasir, A.: Complexity issues in automated synthesis of failsafe fault-tolerance. IEEE Transactions on Dependable and Secure Computing 2, 1–15 (2005)
Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: Logic in Computer Science, pp. 275–284 (2006)
Piterman, N., Pnueli, A., Saár, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005)
Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B. (2010). Robustness in the Presence of Liveness. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)