Record Details

Complete and tractable local linear time temporal logics over traces

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Complete and tractable local linear time temporal logics over traces
 
Creator ADSUL, B
SOHONI, M
 
Subject mazurkiewicz traces
temporal logics
concurrency
mazurkiewicz traces
limits
 
Description 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.
 
Publisher SPRINGER-VERLAG BERLIN
 
Date 2011-10-23T13:56:31Z
2011-12-15T09:11:11Z
2011-10-23T13:56:31Z
2011-12-15T09:11:11Z
2002
 
Type Article; Proceedings Paper
 
Identifier AUTOMATA, LANGUAGES AND PROGRAMMING,2380,926-937
3-540-43864-5
0302-9743
http://dspace.library.iitb.ac.in/xmlui/handle/10054/15147
http://hdl.handle.net/100/1905
 
Source 29th International Colloquium on Automata, Languages and Programming,MALAGA, SPAIN,JUL 08-13, 2002
 
Language English