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

10.29007/3hb9 ◽  
2018 ◽  
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.

scholarly journals Temporalising Separation Logic for Planning with Search Control Knowledge

2017 ◽  
Author(s):  
Xu Lu ◽  
Cong Tian ◽  
Zhenhua Duan
Keyword(s):  
Temporal Logic ◽  
Expressive Power ◽  
Separation Logic ◽  
Temporal Constraints ◽  
Ai Planning ◽  
Temporal Logics ◽  
Spatial Constraints ◽  
Spatio Temporal ◽  
Control Knowledge ◽  
Search Control

Temporal logics are widely adopted in Artificial Intelligence (AI) planning for specifying Search Control Knowledge (SCK). However, traditional temporal logics are limited in expressive power since they are unable to express spatial constraints which are as important as temporal ones in many planning domains. To this end, we propose a two-dimensional (spatial and temporal) logic namely PPTL^SL by temporalising separation logic with Propositional Projection Temporal Logic (PPTL). The new logic is well-suited for specifying SCK containing both spatial and temporal constraints which are useful in AI planning. We show that PPTL^SL is decidable and present a decision procedure. With this basis, a planner namely S-TSolver for computing plans based on the spatio-temporal SCK expressed in PPTL^SL formulas is developed. Evaluation on some selected benchmark domains shows the effectiveness of S-TSolver.

A review of temporal logics

1989 ◽  
Vol 4 (2) ◽  
pp. 141-162 ◽  
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.

Mirror, mirror in my hand: a duality between specifications and models of process behaviour

1996 ◽  
Vol 6 (4) ◽  
pp. 353-373 ◽  
Author(s):  
J. L. Fiadeiro ◽  
J. F. Costa
Keyword(s):  
Temporal Logic ◽  
Structural Property ◽  
Reactive Systems ◽  
Expressive Power ◽  
Seminal Paper ◽  
Process Specification ◽  
Temporal Specifications ◽  
Mirror Mirror

SummarySince Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

scholarly journals Special Issue: Temporal Logic in Engineering

1999 ◽  
Vol 13 (2) ◽  
pp. 65-65
Author(s):  
EPHRAIM NISSAN
Keyword(s):  
Artificial Intelligence ◽  
Petri Nets ◽  
Temporal Logic ◽  
Special Issue ◽  
Temporal Logics ◽  
Modal Operators ◽  
Standard Part ◽  
Temporal Models

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.

scholarly journals Artificial Intelligence along the New Silk Road

2020 ◽  
pp. 240-254
Author(s):  
Lynda Hardman
Keyword(s):  
Artificial Intelligence ◽  
Computer Science ◽  
International Collaboration ◽  
Research Community ◽  
Current Situation ◽  
Silk Road ◽  
Diplomatic Relations ◽  
The Past ◽  
The Usa

Chapter 13 gives an impression of the development of the relatively young AI and computer science fields in Europe and China and how the current situation has developed over the past twenty years, where European and Chinese researchers are equal colleagues on an international stage and where diplomatic relations between the USA and China on the international stage have consequences felt directly by European AI researchers in their labs. In what ways are AI researchers in China and Europe competitors with each other, for example in terms of the global shortage of trained AI researchers and practitioners? At the same time, the AI research community collaborates globally, so how can we ensure that the field continues to benefit from open international collaboration?

scholarly journals Rational verification: game-theoretic verification of multi-agent systems

2021 ◽  
Author(s):  
Alessandro Abate ◽  
Julian Gutierrez ◽  
Lewis Hammond ◽  
Paul Harrenstein ◽  
Marta Kwiatkowska ◽  
...  
Keyword(s):  
Computer Science ◽  
Temporal Logic ◽  
State Of The Art ◽  
Multi Agent System ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
The Past ◽  
Multi Agent ◽  
Game Theoretic ◽  
Temporal Logic Formula

AbstractWe provide a survey of the state of the art of rational verification: the problem of checking whether a given temporal logic formula ϕ is satisfied in some or all game-theoretic equilibria of a multi-agent system – that is, whether the system will exhibit the behavior ϕ represents under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the overall framework of rational verification, we discuss key results obtained in the past few years as well as relevant related work in logic, AI, and computer science.

scholarly journals On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

2021 ◽  
Vol 28 (4) ◽  
pp. 356-371
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Linear Time ◽  
Complete Solution ◽  
Reactive Systems ◽  
Expressive Power ◽  
Regular Languages ◽  
Specification Languages ◽  
Temporal Logics ◽  
Emptiness Problem

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

scholarly journals Pure-Past Linear Temporal and Dynamic Logic on Finite Traces

2020 ◽  
Author(s):  
Giuseppe De Giacomo ◽  
Antonio Di Stasio ◽  
Francesco Fuggitti ◽  
Sasha Rubin
Keyword(s):  
Decision Making ◽  
Dynamic Logic ◽  
Expressive Power ◽  
Decision Problems ◽  
Sequential Decision Making ◽  
Sequential Decision ◽  
The Past ◽  
Temporal Specifications

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf , for computing the corresponding DFA. This exponential improvement is reflected in several forms of sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp., PLDLf ) has the same expressive power as LTLf (resp., LDLf ), but transforming a PLTLf (resp., PLDLf ) formula into its equivalent LTLf (resp.,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf .

Is the Universe a Hologram?

2017 ◽  
Author(s):  
Adolfo Plasencia ◽  
Tim O'Reilly
Keyword(s):  
Artificial Intelligence ◽  
Computer Science ◽  
Quantum Physics ◽  
Physical World ◽  
Human Knowledge ◽  
The Past ◽  
Science Philosophy ◽  
Four Blocks ◽  
Fourth Block ◽  
The Universe

The place of discovery and generation of human knowledge has become a somewhat fuzzy area, and it is at the crossroads of equally blurred disciplines where new glimpses of the future occur. This book looks at these issues through a series of interconnected and heterodox reflections. It is much more a book of non-linear questions than one of answers, where the index consists of a list of questions with those who address the issues linked to them. In 33 dialogues, the author attempts to draw the participants, researchers and creators—each specialists—out of their “intellectual comfort zones”, and get them to delve into areas of disciplines not considered part of their usual activities, thus enabling different concepts to be discussed. For example, “intelligence”, viewed simultaneously from the perspective of neuroscience, computer science, philosophy, and Artificial Intelligence, or whether quantum physics allows for freewill. The diversity and interconnecting ideas in these conversations is wide ranging and intense. The dialogues, preceded by a foreword from Tim O’Reilly, are arranged in four blocks: I, The Physical World; II, Information, and III, Intelligence; the fourth block is a dialogue-epilogue with the artist and painter J. M. Yturralde, closing the book with a critical foray into the overlap between Art and Science, with tantalizing questions, with an artistic slant, such as the validity of the equation “Beauty ≠ Truth,” or whether we can go back in time to the past and change it.

An introduction to executable temporal logics

1996 ◽  
Vol 11 (1) ◽  
pp. 43-56 ◽  
Author(s):  
Michael Fisher
Keyword(s):  
Process Control ◽  
Computer Science ◽  
Programming Languages ◽  
Temporal Logic ◽  
User Interfaces ◽  
Temporal Logics ◽  
Social Modelling ◽  
Basic Concepts ◽  
Direct Execution

In recent years a number of programming languages based upon the direct execution of temporal logic formulae have been developed. The use of such logics provides a powerful basis for the representation and implementation of a range of dynamic behaviours. Though many of these languages are still experimental, they are beginning to be applied, not only in computer science and AI, but also in less obvious areas such as user interfaces, process control and social modelling. This article provides an introduction to some of the basic concepts of executable temporal logics, together with an overview of the main approaches being pursued.

Sign in / Sign up

Export Citation Format

Share Document