Abstract
The Propositional Temporal logic of Linear time (PTL) is often interpreted over sequences (of states or actions) that can be grouped into equivalence classes under a natural partial order based semantics. It has been noticed in the literature that many PTL formulas are consistent with respect to such an equivalence relation. Either all members of an equivalence class satisfy the formula or none of them do. Such formulas can be often verified efficiently. One needs to test satisfiability of the concerned formula for just one member of each equivalence class.
Here we identify an interesting subset of such equivalence consistent PTL formulas — denoted PTL⊗ — by purely semantic means. We then use a partial order based linear time temporal logic denoted TrPTL⊗ to obtain a simple syntactic characterization of PTL⊗. We also provide solutions to the satisfiability problem and an associated model checking problem for TrPTL⊗ using networks of Büchi automata.
This work has been partly supported by the IFCPAR Project 502-1.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Alur, D. Peled and W. Penczek: Model Checking of Causality Properties. To Appear in the Proceedings of the 10th IEEE Symposium on Logic in Computer Science (1995).
V. Diekert, P. Gastin and A. Petit: Rational and Recognizable Complex Trace Languages. Report LITP 92.39, Institut Blaise Pascal, University of Paris, Paris, France (1992).
P. Godefroid and P. Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. LNCS 575, Springer-Verlag Berlin-Amsterdam-New York (1991) 332–343.
S. Katz and D. Peled: Interleaving Set Temporal Logic. Theoretical Computer Science, 73 (3), 21–43, 1992.
A. Mazurkiewicz: Concurrent Program Schemes and their Interpretations. Technical Report DAIMI PB-78, Computer Science Department, Aarhus University, Denmark (1977).
Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems (Specification) Springer-verlag, Berlin (1991).
S. Mahalik and R. Ramanujam: An Axiomatization of Product PTL. Manuscript, The Institute of Mathematical Sciences, Madras (1995).
P. Niebert: A μ-Calculus with Local Views for Systems of Sequential Agents. To Appear in Proc. MFCS'95.
P. Niebert and W. Penczek: On the Connection of Partial Order logics and Partial Order Reduction Methods. Manuscript, 1995.
D. Peled: All from One, One for All: On Model Checking Using Representatives. Proceedings of CAV'93, LNCS 697, 1993.
D. Peled: On Projective and Seperable Properties. Proc. CAAP'94, LNCS 787 (1994).
P.S. Thiagarajan: A Trace based Extension of Linear Time Temporal Logic. Proceedings of 9th IEEE Symposium on Logic in Computer Science, (1994) pp. 438–447.
P.S. Thiagarajan: PTL over Product State Spaces. Report TCS-95-4, School of Mathematics, SPIC Science Foundation, Madras (1995).
A. Valamari: Stubborn Sets for Reduced State Space Generation. LNCS 483 (1990) 491–515.
A. Valamari: A Stubborn Attack on State Explosion. Formal Methods in System Design, 1, 285–313, 1992.
M.Y. Vardi and P. Wolper: An Automata Theoretic Approach to Automatic Program Verification. Proceedings of 1st IEEE Symposium on Logic in Computer Science, (1986) 332–345.
G. Winskel and M. Nielsen: Models for Concurrency. Report DAIMI-PB-429, Computer Science Department, Aarhus University, Aarhus, Denmark (1992). Also to Appear in: Handbook of Logic in Computer Science, Eds: S. Abramsky, D.M. Gabbay and T.S.E. Maibaum.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiagarajan, P.S. (1995). A trace consistent subset of PTL. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_33
Download citation
DOI: https://doi.org/10.1007/3-540-60218-6_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60218-7
Online ISBN: 978-3-540-44738-2
eBook Packages: Springer Book Archive