Abstract
We present the first expressively complete and yet tractable temporal logics, Past-TrLTL and TrLTL, to reason about distributed behaviours, modelled as Mazurkiewicz traces. Both logics admit singly exponential automata-theoretic decision procedures. General formulas of Past-TrLTL are boolean combinations of local formulas which assert rich properties of local histories of the behaviours. Past-TrLTL has the same expressive power as the first order theory of finite traces. TrLTL provides formulas to reason about recurring local Past-TrLTL properties and equals the complete first order theory in expressivity. The expressive completeness criteria are based on new local normal forms for the first order logic. We illustrate the use of our logics for specification of global properties.
The work of this author was supported by an Infosys Fellowship.
This is a preview of subscription content, log in via an institution to check access.
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. Adsul AND M. Sohoni: First-Order Logic over Traces, Technical Report, Dept. of Computer Science & Engineering, I. I. T. Mumbai, India (2002). Also see http://www.cse.iitb.ac.in/~abharat/logics.html
V. Diekert AND P. Gastin: LTL is Expressively Complete for Mazurkiewicz Traces, Proc. ICALP’ 00, LNCS 1853 (2000) 211–222.
V. Diekert AND P. Gastin: Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets, Proc. LPAR’ 01, LNAI 2250 (2000) 55–69.
V. Diekert AND A. Muscholl: Deterministic Asynchronous Automata for Infinite Traces, Acta Inf., 31 (1993) 379–397.
V. Diekert AND G. Rozenberg (Eds.): The Book of Traces, World Scientific, Singapore (1995).
W. Ebinger AND A. Muscholl: Logical Definability on Infinite Traces, Proc. ICALP’ 93, LNCS 700 (1993) 335–346.
O. Maler AND A. Pnueli: Tight bounds on the Complexity of Cascaded Decomposition of Automata, Proc. 31st IEEE FOCS’ 90 (1990) 672–682.
Z. Manna AND A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems (Specification), Springer-Verlag, Berlin (1991).
R. McNaughton AND S. Papert: Counter-free Automata, MIT Press, Cam-bridge (1971).
M. Mukund AND M. Sohoni: Keeping Track of the Latest Gossip in a Distributed System, Distributed Computing, 10(3) (1997) 137–148.
M. Mukund AND P.S. Thiagarajan: Linear Time Temporal Logics over Mazurkiewicz Traces, Proc. MFCS’96, LNCS 1113 (1996) 62–92.
P.S. Thiagarajan: A Trace Based Extension of Linear Time Temporal Logic, Proc. 9th IEEE LICS (1994) 438–447.
W. Thomas: Languages, Automata and Logic, in: Handbook of Formal Languages Vol. 3 — Beyond Words, Springer-Verlag, New York (1997) 389–456.
P.S. Thiagarajan AND I. Walukiewicz: An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces, Proc. 12th IEEE LICS (1997) 183–194.
I. Walukiewicz: Difficult Configurations-On the Complexity of LTrL, Proc. ICALP’ 98, LNCS 1443 (1998) 140–151.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adsul, B., Sohoni, M. (2002). Complete and Tractable Local Linear Time Temporal Logics over Traces. In: Widmayer, P., Eidenbenz, S., Triguero, F., Morales, R., Conejo, R., Hennessy, M. (eds) Automata, Languages and Programming. ICALP 2002. Lecture Notes in Computer Science, vol 2380. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45465-9_79
Download citation
DOI: https://doi.org/10.1007/3-540-45465-9_79
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43864-9
Online ISBN: 978-3-540-45465-6
eBook Packages: Springer Book Archive