Gastin, Paul ; Mukund, Madhavan (2002) An elementary expressively complete temporal logic for Mazurkiewicz traces In: 29th International Colloquium on Automata, Languages, and Programming (ICALP 2002), 08-13, July 2002, Málaga, Spain.
Full text not available from this repository.
Official URL: https://link.springer.com/chapter/10.1007%2F3-540-...
Related URL: http://dx.doi.org/10.1007/3-540-45465-9_80
Abstract
In contrast to the classical setting of sequences, no temporal logic has yet been identified over Mazurkiewicz traces that is equivalent to first-order logic over traces and yet admits an elementary decision procedure. In this paper, we describe a local temporal logic over traces that is expressively complete and whose satisfiability problem is in Pspace. Contrary to the situation for sequences, past modalities are essential for such a logic. A somewhat unexpected corollary is that first-order logic with three variables is expressively complete for traces.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Source: | Copyright of this article belongs to Springer-Verlag. |
| Keywords: | Temporal Logics; Mazurkiewicz Traces; Concurrency |
| ID Code: | 114210 |
| Deposited On: | 25 May 2018 04:53 |
| Last Modified: | 25 May 2018 04:53 |
Repository Staff Only: item control page
