Describing properties of concurrent systems (Logic for Traces) (invited talk)

AbstractMazurkiewicz traces are one of the simplest non-interleaving model of executions. For some systems the trace model may be exponentially smaller than the transition system model. This is one of the motivations for studying formalisms describing directly the properties of traces. Traces have also very nice theoretical properties. For example, there are characterizations of first-order definable and monadic second order definable (i.e. regular) languages and these characterizations are very similar to the ones in the case of words.Our goal is to find formalism that have the same expressive power as first or monadic-second order logic but that are manageable at the same time (i.e. with satisfiability and model checking problems in PSPACE). In other words, we want to understand what can be LTL and the mu-calculus variants for traces.A temporal logic over trace is called local if the meaning of a formula is a set of positions in the trace. A logic is called global if the meaning of a formula is a set of configurations (finite downwards closed subsets of positions). We will survey the results on both kind of logics. Among global logics it is relatively easy to find an expressively complete formalism but these logics have high complexity. Somewhat surprisingly there exist local expressively complete logics. Unfortunately, the presently known formalisms require some operators that are not completely satisfactory