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. © 2002 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Adsul, B., & Sohoni, M. (2002). Complete and tractable local linear time temporal logics over traces. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2380 LNCS, pp. 926–937). Springer Verlag. https://doi.org/10.1007/3-540-45465-9_79
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
