Since 2014
A Product Version of Dynamic Linear Time Temporal Logic
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
A Product Version of Dynamic Linear Time Temporal Logic
|
|
| Creator |
Henriksen, Jesper G.
Thiagarajan, P. S. |
|
| Description |
We present here a linear time temporal logic which simultaneously extends LTL, the propositional temporal logic of linear time, along two dimensions. Firstly, the until operator is strengthened by indexing it with the regular programs of propositional dynamic logic (PDL). Secondly, the core formulas of the logic are decorated with names of sequential agents drawn from fixed finite set. The resulting logic has a natural semantics in terms of the runs of a distributed program consisting of a finite set of sequential programs that communicate by performing common actions together. We show that our logic, denoted DLTL, admits an exponential time decision procedure. We also show that DLTL is expressively equivalent to the so called regular product languages.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-09
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18800
10.7146/brics.v4i9.18800 |
|
| Source |
BRICS Report Series; No 9 (1997): RS-09 A Product Version of Dynamic Linear Time Temporal Logic
BRICS Report Series; Nr. 9 (1997): RS-09 A Product Version of Dynamic Linear Time Temporal Logic 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18800/16445
|
|