Special Issue: Temporal Logic in Engineering

Logic-based models are thriving within artificial intelligence. A great number of new logics have been defined, and their theory investigated. Epistemic logics introduce modal operators for knowledge or belief; deontic logics are about norms, and introduce operators of deontic necessity and possibility (i.e., obligation or prohibition). And then we have a much investigated class—temporal logics—to whose application to engineering this special issue is devoted. This kind of formalism deserves increased widespread recognition and application in engineering, a domain where other kinds of temporal models (e.g., Petri nets) are by now a fairly standard part of the modelling toolbox.

Download Full-text

A review of temporal logics

The Knowledge Engineering Review ◽

10.1017/s0269888900004896 ◽

1989 ◽

Vol 4 (2) ◽

pp. 141-162 ◽

Cited By ~ 6

Author(s):

Derek Long

Keyword(s):

Artificial Intelligence ◽

Temporal Logic ◽

Temporal Reasoning ◽

Order Logic ◽

First Order Logic ◽

Temporal Logics ◽

Detailed Review ◽

First Order ◽

Reasoning Tasks

AbstractA series of temporal reasoning tasks are identified which motivate the consideration and application of temporal logics in artificial intelligence. There follows a discussion of the broad issues involved in modelling time and constructing a temporal logic. The paper then presents a detailed review of the major approaches to temporal logics: first-order logic approaches, modal temporal logics and reified temporal logics. The review considers the most significant exemplars within the various approaches, including logics due to Russell, Hayes and McCarthy, Prior, McDermott, Allen, Kowalski and Sergot. The logics are compared and contrasted, particularly in their treatments of change and action, the roles they seek to fulfil and the underlying models of time on which they rest. The paper concludes with a brief consideration of the problem of granularity—a problem of considerable significance in temporal reasoning, which has yet to be satisfactorily treated in a temporal logic.

Download Full-text

A One-Pass Tree-Shaped Tableau for LTL+Past

10.29007/3hb9 ◽

2018 ◽

Cited By ~ 1

Author(s):

Nicola Gigante ◽

Angelo Montanari ◽

Mark Reynolds

Keyword(s):

Artificial Intelligence ◽

Computer Science ◽

Temporal Logic ◽

Expressive Power ◽

Temporal Constraints ◽

Temporal Logics ◽

The Past ◽

Tableau System ◽

Standard Formalism ◽

Temporal Specifications

Linear Temporal Logic (LTL) is a de-facto standard formalism for expressing properties of systems and temporal constraints in formal verification, artificial intelligence, and other areas of computer science. The problem of LTL satisfiability is thus prominently important to check the consistency of these temporal specifications. Although adding past operators to LTL does not increase its expressive power, recently the interest for explicitly handling the past in temporal logics has increased because of the clarity and succinctness that those operators provide. In this work, a recently proposed one-pass tree-shaped tableau system for LTL is extended to support past operators. The modularity of the required changes provides evidence for the claimed ease of extensibility of this tableau system.

Download Full-text