Abstract
Requirements of reactive systems are usually specified by classifying system executions as desirable and undesirable. To specify prioritized requirements, we propose to associate a rank with each execution. This leads to optimization analogs of verification and synthesis problems in which we compute the “best” requirement that can be satisfied or enforced from a given state. The classical definitions of acceptance criteria for automata can be generalized to ranking conditions. In particular, given a mapping of states to colors, the Büchi ranking condition maps an execution to the highest color visited infinitely often by the execution, and the cyclic ranking condition with cycle k maps an execution to the modulo-k value of the highest color repeating infinitely often. The well-studied parity acceptance condition is a special case of cyclic ranking with cycle 2, and we show that the cyclic ranking condition can specify all ω-regular ranking functions. We show that the classical characterizations of acceptance conditions by fixpoints over sets generalize to characterizations of ranking conditions by fixpoints over an appropriately chosen lattice of coloring functions. This immediately leads to symbolic algorithms for solving verification and synthesis problems. Furthermore, the precise complexity of a decision problem for ranking conditions is no more than the corresponding acceptance version, and in particular, we show how to solve Büchi ranking games in quadratic time.
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
Alur, R., Etessami, K., Torre, S.L., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Log 2(3), 388–407 (2001)
Bruns, G., Godefroid, P.: Model Checking with Multi-valued Logics. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer, Heidelberg (2004)
Buttazzo, G.: Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications. Kluwer Academic Publishers, Boston, USA (2000)
Chatterjee, K.: A linear-time algorithm for weak parity games. Technical Report UCB/EECS-2006-153, University of California, Berkeley (2006)
Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In: Proc. 3rd Conference on Computer Aided Verification, pp. 48–58 (1991)
Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier Science Publishers, Amsterdam (1990)
Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for the μ-calculus and its fragments. Theor. Comput. Sci 258(1-2), 491–522 (2001)
Ernits, J.P.: Memory arbiter synthesis and verification for a radar memory interface card. Nord. J. Comput 12(2), 68–88 (2005)
Gimbert, H., Zielonka, W.: Perfect information stochastic priority games. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 850–861. Springer, Heidelberg (2007)
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Proc. 14th Annual ACM Symposium on Theory of Computing, pp. 60–65 (1982)
Büchi, J.R.: State-strategies for games in F σδ ∩ G σδ . Journal of Symbolic Logic 48, 1171–1198 (1983)
Kupferman, O., Lustig, Y.: Lattice automata. In: Proc. 8th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, pp. 199–213 (2007)
Kupferman, O., Lustig, Y.: Latticed simulation relations and games. In: Proc. 5th symp. on Aut. Technology for Verification and Analysis, pp. 316–330 (2007)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symposium on Foundations of Computer Science, pp. 46–77 (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symposium on Principles of Programming Languages (1989)
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic Decision Diagrams and Their Applications. In: Proc. 9th International Conference on CAD, pp. 188–191 (1993)
Thomas, W.: On the synthesis of strategies in infinite games. In: Proc. 12th Symp. on Theoretical Aspects of Computer Science, pp. 1–13 (1995)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
Weiss, G.: Optimal scheduler for a memory card. Research report, Dep. of Computer Science and Applied Mathematics, The Weizmann Institue of Science (2002)
Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1-2), 343–359 (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Kanade, A., Weiss, G. (2008). Ranking Automata and Games for Prioritized Requirements. In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)