Abstract
Bounded model checking methodologies check the correctness of a system with respect to a given specification by examining computations of a bounded length. Results from set-theoretic topology imply that sets in Σω that are both open and closed (clopen sets) are precisely bounded sets: membership of a word in a clopen set can be determined by examining a bounded prefix of it. Clopen sets correspond to specifications that are both safety and co-safety. In this paper we study bounded specifications from this perspective. We consider both the linear and the branching frameworks. In the linear framework, we show that when clopen specifications are given by word automata or temporal logic formulas, we can identify a bound and translate the specification to bounded formalisms such as cycle-free automata and bounded LTL. In the branching framework, we show that while clopen sets of trees with infinite branching degrees may not be bounded, we can extend the results from the linear framework to clopen specifications given by tree automata or temporal logic formulas, even for trees with infinite branching degrees. There, we can identify a bound and translate clopen specifications to cycle-free automata and modal logic. Finally, we show how our results imply that the bottom levels of the μ-calculus hierarchy coalesce.
Supported in part by BSF grant 9800096.
Supported in part by NSF grants CCR-9700061, CCR-9988322, IIS-9908435, IIS-9978135, and EIA-0086264 by BSF grant 9800096, and by a grant from the Intel Corporation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Alpern and F.B. Schneider. Defining liveness. IPL, 21:181–185, 1985.
B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed computing, 2:117–126, 1987.
J. Benthem and J. Bergstra. Logic of transition systems. Technical Report P9308, Programing research group, University of Amsterdam, 1993.
A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. 36th DAC, pp. 317–320, 1999.
A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In TACAS, LNCS 1579, 1999.
A. Biere, E.M. Clarke, R. Raimi, and Y. Zhu. Verifying safety properties of a PowerPC[tm] microprocessor using symbolic model checking without BDDs. In Proc. 11th CAV, LNCS 1633, pp. 172–183, 1999.
J. Benthem. Languages in actions: categories, lambdas and dynamic logic. Studies in Logic, 130, 1991.
A. Bouajjani, J.-C. Fernandez, S. Graf, C. Rodriguez, and J. Sifakis. Safety for branching semantics. In Proc. 18th ICALP, LNCS, pp. 76–92, 1991.
R. Bloem, H.N. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. In FMCAD, LNCS 1954, pp. 37–54, 2000.
J. Barwise and Y.N. Moschovakis. Global inductive definability. Journal of Symbolic Logic, 43(3):521–534, 1978.
J.C. Bradfield. The modal μ-calculus alternation hierarchy is strict. Theoretical Computer Science, 195(2):133–153, March 1998.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. JACM, 33(1):151–178, 1986.
E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proc. 1st LICS, pp. 267–278, 1986.
E.A. Emerson. Alternative semantics for temporal logics. Theoretical Computer Science, 26:121–130, 1983.
M. Garey and D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-completeness. W. Freeman and Co., San Francisco, 1979.
H.P. Gumm. Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions. IPL, 47:291–294, 1993.
R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi. A new heuristic for bad cycle detection using BDDs. In Proc. 9th CAV, LNCS 1254, pp. 268–278, 1997.
H.J. Hoogeboom and G. Rozenberg. Infinitary languages: basic theory and applications to concurrent systems. In Proc. Advanced School on Current Trends in Concurrency, LNCS 224, pp. 266–342, 1986.
D. Janin and I. Walukiewicz. Automata for the modal μ-calculus and related results. In Proc. 20th MFCS, LNCS, pp. 552–562, 1995.
E. Kindler. Safety and liveness properties: A survey. EATCS, 53:268–272, 1994.
D. Kozen. Results on the propositional μ-calculus. TCS, 27:333–354, 1983.
R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.
O. Kupferman and M.Y. Vardi. Model checking of safety properties. In Proc. 11th CAV, LNCS 1633, pp. 172–183, 1999.
O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. JACM, 47(2):312–360, March 2000.
L. Lamport. Sometimes is sometimes “not never”-on the temporal logic of programs. In Proc. 7th POPL, pp. 174–185, 1980.
L. Lamport. Logical foundation. In Distributed systems-methods and tools for specification, LNCS 190, 1985.
L.H. Landweber. Decision problems forω-automata. Mathematical Systems Theory, 3:376–384, 1969.
S. Miyano and T. Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32:321–330, 1984.
Z. Manna and A. Pnueli. The anchored version of the temporal framework. In Linear time, branching time, and partial order in logics and models for concurrency, LNCS 345, pp. 201–284, 1989.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification., Berlin, January 1992.
P. Manolios and R. Trefler. Safety and liveness in branching time. In Proc. 16th LICS, 2001.
D. Niwiński. On fixed point clones. In Proc. 13th ICALP, LNCS 226, pp. 464–473, 1986.
M. Otto. Eliminating recursion in the μ-calculus. In Proc. 16th STACS, LNCS 1563, pp. 531–540, 1999.
M.O. Rabin and D. Scott. Finite automata and their decision problems. IBM Journal of Research and Development, 3:115–125, 1959.
C.J.H. Seger and R.E. Bryant. Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design, 6:147–189, 1995.
A.P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6:495–511, 1994.
L. Staiger. ω-languages. Handbook of Formal Languages, pp. 339–388, 1997.
W. Thomas. Automata on infinite objects. Handbook of Theoretical Computer Science, pp. 165–191, 1990.
M.Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pp. 238–266, 1996.
M.Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Science, 32(2):182–221, April 1986.
M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, November 1994.
T. Wilke. CTL+ is exponentially more succinct than CTL. In Proc. 19th FST&TCS, 1738, pp. 110–121, 1999.
T. Wilke. Classifying discrete temporal properties In Proc. 16th STACS, LNCS 1563, pp. 32–46, 1999.
J. Yang. A theory for generalized symbolic trajectory evaluation. In Symposium on Symbolic Trajectory Evaluation, Chicago, July 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Vardi, M. (2001). On Bounded Specifications. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_2
Download citation
DOI: https://doi.org/10.1007/3-540-45653-8_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42957-9
Online ISBN: 978-3-540-45653-7
eBook Packages: Springer Book Archive