loading...
Model-checking Trace Event Structures
Ottawa, Canada June 22-June 25
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2003.121007718th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
P. Madhusudan, University of Pennsylvania
Given a regular collection of Mazurkiewicz traces, which can be seen as the behaviours of a finite-state concurrent system, one can associate with it a canonical regular event structure. This event structure is a single (often infinite) structure that captures both the concurrency and conflict information present in the system. We study the problem of model-checking such structures against logics such as first-order logic (FOL), monadic second-order logic (MSOL) and a new logic that lies in between these two called monadic trace logic (MTL). MTL is a fragment of MSOL where the quantification is restricted to sets that are conflict-free. While it is known that model-checking such event structures against MSOL is undecidable, our main results are that FOL and MTL admit effective model-checking procedures. It turns out that FOL captures previously known decidable temporal logics on event structures. MTL is more powerful and can express interesting branching-time properties of event structures, and when restricted to a sequential setting, can express the standard logic CTL* over trees.
Citation:
P. Madhusudan, "Model-checking Trace Event Structures," lics, pp.371, 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.