Abstract
We define a logic called CTL*[DC] which extends CTL* with ability to specify past-time and quantitative timing properties using the formulae of Quantified Discrete-time Duration Calculus (QDDC). Alternately, we can consider CTL*[DC] as extending logic QDDC with branching and liveness.
As our main result, we show a reduction of CTL*[DC] model checking problem to model checking of CTL* formulae. The reduction relies upon an automata-theoretic decision procedure for QDDC. Moreover, it preserves the subsets CTL and LTL of CTL*. The reduction is of practical relevance as model checking of CTL* as well as its subsets CTL and LTL are well studied and even implemented into a number of tools. We briefly discuss an implementation of a model checking tool for CTL[DC] called CTLDC, based on the above theory. CTLDC can model check SMV, Verilog and Esterel designs using tools SMV, VIS and Xeve, respectively.
Partially supported by the UNU/IIST offshore project Semantics and verification of real-time programs using Duration Calculus: Theory and Practice
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
A. Bouali, XEVE: An Esterel Verification Environment, Proc. Computer Aided Verification, CAV’98, Lecture Notes in Computer Science, Springer-Verlag, 1998.
R.K. Bryton, G.D. Hatchtel et al, VIS: A system for verification and synthesis, in Proc. Computer Aided Verification, CAV’96, Lecture Notes in Computer Science 1102, Springer-Verlag, 1996.
J.R. Buchi, Weak second-order arithmetic and finite automata, Z. Math. Logik Grundl. Math. 6, 1960.
E.M. Clarke and E.A. Emerson, Synthesis of synchronisation skeletons for branching time temporal logic, Proc. Logics of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.
E.M. Clarke, E.A. Emerson and A.P. Sistla, Automatic verification of finite-stateconcurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, 8(2), 1986.
A. Cimatti, E.M. Clarke, F. Giunchiglia and M. Roveri, NuSMV: A Reimplementation of SMV, Proc. International Workshop on Software Tools for Technology Transfer (STTT-98), BRICS Notes Series, NS-98-4, 1998.
C.C. Elgot, Decision problems of finite automata design and related arithmetics, Trans. Amer. Math. Soc. 98, 1961.
E.A. Emerson and C-L. Lei, Modalities for Model checking: Branching time strikes back, 12th Symposium on Principles of Programming Languages, New Orleans, La., (January) 1985.
E.A. Emerson, A.K. Mok, A.P. Sistla and J. Srinivasan, Quantitative temporal reasoning, Proc. Computer Aided Verification,CAV’90, Lecture Notes in Computer Science 531, Springer-Verlag, 1991.
M.R. Hansen and Zhou Chaochen, Duration Calculus: Logical Foundations, Journal of Formal Aspects of Computing 9, 1997.
J.G. Henriksen, J. Jensen, M. Jorgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm, Mona: Monadic Second-Order Logic in Practice, Proc. Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS’ 95, Lecture Notes in Computer Science 1019, 1996.
Y. Kesten, A. Pnueli, and L. Raviv, Algorithmic Verification of Linear Temporal Logic Specifications, in Proc. 25th International Colloquium on Automata, Languages, and Programming, ICALP’98, Lecture Notes in Computer Science 1443, Springer-Verlag, 1998.
N. Klarlund, A. Mø ller and M.I. Schwartzbach, MONA Implementation Secrets, to appear in Proc. Fifth Conference on Implementation and Application of Automata, CIAA 2000, Springer-Verlag, 2000.
O. Kupferman and A. Pnueli, Once and for all, in proc. 10th IEEE Symposium on Logics in Computer Science, LICS’95, San Diago, June 1995.
F. Laroussinie and P. Schnoebelen, A Hierarchy of Temporal Logics with Past, Theoretical Computer Science, 140(1), 1995.
O. Lichtenstein and A. Pnueli, Checking that Finite State Concurrent Programs Satisfy Their Linear Specification. In Prof. 12 ACM Symposium on Principles of Prog. Languages, POPL’85, January 1985.
O. Lichtenstein, A. Pnueli and L. Zuck, The Glory of the Past, Proc. Logics of Programs, Lecture Notes in Computer Science 193, Springer-Verlag, 1985.
K. McMillan, Symbolic Model Checking, Kluwer Academic Publisher, 1993.
B. Moszkowski, A Temporal Logic for Multi-Level Reasoning about Hardware, IEEE Computer, 18(2), 1985.
P.K. Pandya, Some Extensions to Mean-Value Calculus: Expressiveness and Decidability, Proc. Computer Science Logic, CSL’95, Paderborn, Germany, Lecture Notes in Computer Science 1092, Springer-Verlag, 1996.
P.K. Pandya, DCVALID User Manual, Tata Institute of Fundamental Research, Bombay, 1997. (Available in revised version at http://www.tcs.tifr.res.in/~pandya/dcvalid.html)
P.K. Pandya, Specifying and Deciding Quantified Discrete-time Duration Calculus Formulae using DCVALID: An Automata Theoretic Approach, Technical Report TCS-00-PKP-1, Tata Institute of Fundamental Research, 2000.
P.K. Pandya, Model Checking CTL[DC] properties of SMV, Verilog and Esterel Designs using CTLDC, Technical Report TCS-00-PKP-3, Tata Institute of Fundamental Research, September 2000.
P.K. Pandya, Examples of complex properties from VIS literature, Technical Note PKP-TN-2000-02, Computer Science Group, Tata Institute of Fundamental Research, July 2000. Available on Web at http://www.tcs.tifr.res.in/~pandya/dccheck/demo/sample.html.
A. Pnueli, The Temporal Logic of Programs, Proc. 18th IEEE Symposium on Foundations of Computer Science, 1977.
Zhou Chaochen, C.A.R. Hoare and A.P. Ravn, A Calculus of Durations, Info. Proc. Letters, 40(5), 1991.
Zhou Chaochen, M.R. Hansen, A.P. Ravn and H. Rischel, Duration Specification for Shared Processors, Proc. Formal Techniques in Real-Time and Fault-Tolerent Computing, FTRTFT’92, Lecture Notes in Computer Science 571, Springer-Verlag, 1992.
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
Pandya, P.K. (2001). Model Checking CTL*[DC]. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_38
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive