Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

Paper: Model-checking Trace Event Structures (at LICS 2003)

Authors: Parthasarathy Madhusudan

Abstract

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.

BibTeX

  @InProceedings{Madhusudan-ModelcheckingTraceE,
    author = 	 {Parthasarathy Madhusudan},
    title = 	 {Model-checking Trace Event Structures},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003)},
    year =	 {2003},
    month =	 {June}, 
    pages =      {371--380},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski