Abstract
Liveness properties of on-going reactive systems assert that something good will happen eventually. In satisfying liveness properties, there is no bound on the “wait time”, namely the time that may elapse until an eventuality is fulfilled. The traditional “unbounded” semantics of liveness properties nicely corresponds to the classical semantics of automata on infinite objects. Indeed, acceptance is defined with respect to the set of states the run visits infinitely often, with no bound on the number of transitions taken between successive visits.
In many applications, it is important to bound the wait time in liveness properties. Bounding the wait time by a constant is not always possible, as the bound may not be known in advance. It may also be very large, resulting in large specifications. Researchers have studied prompt eventualities, where the wait time is bounded, but the bound is not known in advance. We study the automata-theoretic counterpart of prompt eventually. In a prompt-Büchi automaton, a run r is accepting if there exists a bound k such that r visits an accepting state every at most k transitions. We study the expressive power of nondeterministic and deterministic prompt-Büchi automata, their properties, and decision problems for them. In particular, we show that regular nondeterministic prompt Büchi automata are exactly as expressive as nondeterministic co-Büchi automata.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Alpern, B., Schneider, F.B.: Defining liveness. IPL 21, 181–185 (1985)
Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for model measuring. ACM Transactions on Computational Logic 2(3), 388–407 (2001)
Alur, R., Henzinger, T.A.: Finitary fairness. In: Proc. 9th IEEE Symp. on Logic in Computer Science, pp. 52–61 (1994)
Bojanczyk, M.: A bounding quantifier. In: Proc. 13th Annual Conf. of the European Association for Computer Science Logic, pp. 41–55 (2004)
Bojańczyk, M., Colcombet, T.: Bounds in ω-regularity. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 285–296 (2006)
Boker, U., Kupferman, O.: Co-ing Büchi made tight and helpful. In: Proc. 24th IEEE Symp. on Logic in Computer Science, pp. 245–254 (2009)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science, pp. 1–12 (1962)
Chatterjee, K., Henzinger, T.A.: Finitary winning in ω-regular games. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 257–271. Springer, Heidelberg (2006)
Derahowitz, N., Jayasimha, D.N., Park, S.: Bounded fairness. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 304–317. Springer, Heidelberg (2004)
Horn, F.: Faster algorithms for finitary games. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 472–484. Springer, Heidelberg (2007)
Jones, N.D.: Space-bounded reducibility among combinatorial problems. Journal of Computer and Systems Science 11, 68–75 (1975)
Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic ω-automata vis-a-vis deterministic Büchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994)
Kupferman, O., Morgenstern, G., Murano, A.: Typeness for ω-regular automata. IJFCS 17(4), 869–884 (2006)
Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)
Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 406–419. Springer, Heidelberg (2007)
Kupferman, O., Vardi, M.Y.: Verification of fair transition systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 372–382. Springer, Heidelberg (1996)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)
Landweber, L.H.: Decision problems for ω–automata. Mathematical Systems Theory 3, 376–384 (1969)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Margaria, T., Sistla, A.P., Steffen, B., Zuck, L.D.: Taming interface specifications. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 548–561. Springer, Heidelberg (2005)
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
Almagor, S., Hirshfeld, Y., Kupferman, O. (2010). Promptness in ω-Regular Automata. In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-15643-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15642-7
Online ISBN: 978-3-642-15643-4
eBook Packages: Computer ScienceComputer Science (R0)