A product version of dynamic linear time temporal logic

10Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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. Roughly speaking, this class of languages is obtained by starting with synchronized products of (ω-)regular languages and closing under boolean operations. We also sketch how the behaviours captured by our temporal logic fit into the framework of labelled partial orders known as Mazurkiewicz traces.

Cite

CITATION STYLE

APA

Henriksen, J. G., & Thiagarajan, P. S. (1997). A product version of dynamic linear time temporal logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1243, pp. 45–58). Springer Verlag. https://doi.org/10.1007/3-540-63141-0_4

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free