Abstract
When verifying concurrent systems described by transition systems, state explosion is one of the most serious problems. If quantitative temporal information (expressed by clock ticks) are considered,state explosion is even more serious. In this paper we present a non-standard (abstract) semantics for the ASTP language able to produce reduced transition systems. The important point is that the abstract semantics produces transition systems equivalent to the standard ones for what concerns the satisfiability of a given set of formulae of a temporal logic with quantitative modal operators. The equivalence of transition systems with respect to formulae is expressed by means of 〈ρ,η〉-equivalence: two 〈ρ,η〉-equivalent transition systems give the same truth value to all formulae such that the actions occurring in the modal operators are contained in ρ, and with time constraints whose values are less than or equal to η.
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
L. Aceto, A. Burgueño, K.G. Larsen. Model Checking via Reachability Testing for Timed Automata. In Proceedings of TACAS’98, Lecture Notes in Computer Science 1384, 1998. 263–280.
R. Alur, T.A. Henzinger. Logics and Models of Real Time: A Survey. In Proceedings of Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, 1991. 74–106.
R. Alur, T.A. Henzinger. A Really Temporal Logic. J. ACM, 41(1), 1994. 181–204.
R. Barbuti, N. De Francesco, A. Santone, G. Vaglini. Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems. In Proceedings of FORTE X/PSTV XVII’ 97. Chapman x0026; Hall, 1997. 519–534.
R. Barbuti, N. De Francesco, A. Santone, G. Vaglini. Selective mu-calculus and Formula-Based Equivalence of Transition Systems. To appear on Journal of Computer and System Sciences, 1999.
S. Bensalem, A. Bouajjani, C. Loiseaux, J. Sifakis. Property Preserving Simulations. In Proceedings of Workshop on Computer Aided Verification (CAV’92), Lecture Notes in Computer Science 663, 1992. 260–273.
J. Bradfield, C. Stirling. Verifying Temporal Properties of Processes. In Proceedings of International Conference on Concurrency Theory (CONCUR’90), Lecture Notes in Computer Science 458, 1990. 115–125.
E.M. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite-state Concurrent Systems using Temporal Logic Verification. ACM Transactions on Programming Languages and Systems, 8, 1986. 244–263.
E.M. Clarke, O. Grumberg, D.E. Long. Model Checking and Abstraction. ACM Transactions on Programming Languages and Systems, 16, 1992. 343–354.
R. Cleaveland, S. Sims. The NCSU Concurrency Workbench. In Proceedings of Workshop on Computer Aided Verification (CAV’96), Lecture Notes in Computer Science 1102, 1996. 394–397.
D. Dams, O. Grumberg, R. Gerth. Generation of Reduced Models for Checking Fragments of CTL. In Proceedings of Workshop on Computer Aided Verification (CAV’93), Lecture Notes in Computer Science 697, 1993. 479–490.
D. Dams, O. Grumberg, R. Gerth. Abstract Interpretation of Reactive Systems. ACM Transaction of Programming Languages and Systems, 19, 1997. 253–291.
R. De Simone, D. Vergamini. Aboard AUTO. INRIA Technical Report 111, 1989.
E.A. Emerson. Real-Time and the Mu-Calculus. In Proceedings of Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, 1991. 176–194.
E.A. Emerson, R.F. Trefler. Generalized Quantitative Temporal Reasoning: An Automata-Theoretic Approach. In Proceedings of TAPSOFT’97, Lecture Notes in Computer Science 1214, 1997. 189–200.
J.C. Fernandez et al. CADP A Protocol Validation and Verification Toolbox. In Proceedings of the Third International Conference on Computer-Aided Verification, Lecture Notes in Computer Science 1102, 1996. 437–440
G. Juanole, L. Gallon. Concept of Quantified Abstract Quotient Automaton and its advantage. In Proceedings of FORTE X/PSTV XVII’ 97. Chapman& Hall, 1997. 223–238.
T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for real-time Systems. Information and Computation, 111, 1994. 193–244.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983. 333–354.
F. Laroussinie, K.G. Larsen, C. Weise. From Timed Automata to Logic-and Back. In Proceedings of MFCS’95, Lecture Notes in Computer Science 969, 1995. 529–538.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
X. Nicollin, J. Sifakis. The Algebra of Timed Processes, ATP: Theory and Application. Information and Computation, 114, 1994. 131–178.
O.V. Sokolsky, S.A. Smolka. Local Model Checking for Real-Time Systems. In Proceedings of Workshop on Computer Aided Verification (CAV’95), Lecture Notes in Computer Science 939, 1995. 211–224.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbuti, R., De Francesco, N., Santone, A., Vaglini2, G. (1999). Formula Based Abstractions of Transition Systems for Real-Time Model Checking. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_18
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive