Abstract
We investigate local and global paradigms of reasoning about distributed behaviours, modelled as Mazurkiewicz traces, in the context of first-order and monadic second-order logics. We describe new normal forms for properties expressible in these logics. The first normal form, surprisingly, yields a decomposition of a global property as a boolean combination of local properties. The second normal form strengthens McNaughton’s theorem and states that global properties of infinite behaviours may also be described as boolean combinations of recurring properties of finite local histories of the behaviours. We briefly touch upon some of the interesting applications of these normal forms.
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.
References
B. Adsul and M. Sohoni: Complete and Tractable Local Linear Time Temporal Logics over Traces, Proc. ICALP’ 02, LNCS 2380 (2002) 926–937.
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 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).
H.-D. Ebbinghaus and J. Flum: Finite Model Theory, Springer-Verlag, NewYork (1995).
W. Ebinger and A. Muscholl: Logical Definability on Infinite Traces, Proc. ICALP’ 93, LNCS 700 (1993) 335–346.
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.
W. Thomas: On Logical Definability of Trace Languages, Proc. an ASMICS workshop, Report TUM-I9002, Technical Univ. of Munich, (1989) 172–182.
W. Thomas: Automata on Infinite Objects, in: Handbook of Theoretical Computer Science Vol. B, Elsevier, Amsterdam (1990) 135–191.
I. Walukiewicz: Difficult Configurations-On the Complexity of LTrL, Proc. ICALP’ 98, LNCS 1443 (1998) 140–151.
W. Zielonka: Notes on Finite Asynchronous Automata, RAIRO Inform. Théor. Appl. 21 (1987) 99–135.
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). Local Normal Forms for Logics over Traces. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_6
Download citation
DOI: https://doi.org/10.1007/3-540-36206-1_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00225-3
Online ISBN: 978-3-540-36206-7
eBook Packages: Springer Book Archive