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.

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 Ruina/basural: Lógicas temporales y espaciales de la ciudad de La Paz en Saenz y Viscarra

2021 ◽  
Vol 26 ◽  
pp. 158-180
Author(s):  
Irina Alexandra Feldman
Keyword(s):  
Temporal Logic ◽  
Linear Temporal Logic ◽  
Space Time ◽  
Victor Hugo ◽  
National Narrative ◽  
Temporal Logics ◽  
La Paz ◽  
Queer Space ◽  
Spatio Temporal ◽  
The City

This article analyzes spatio-temporal logics in the representation of the city of La Paz in Imágenes Paceñas by Jaime Saenz and the urban chronicles of Víctor Hugo Viscarra. Juxtaposing the concepts of chrononormativity and queer time, it explores how linear temporal logic remains insufficient for the understanding of the city and its inhabitants in the two narrative projects. The article postulates that the marginal spaces of architectural ruins and garbage dumps, and the marginalized people who inhabit queer space-time are key to “revealing the hidden city” and understanding its contradictory place in the national narrative and space.

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 Combining Spatial and Temporal Logics: Expressiveness vs. Complexity

2005 ◽  
Vol 23 ◽  
pp. 167-243 ◽  
Author(s):  
D. Gabelaia ◽  
R. Kontchakov ◽  
A. Kurucz ◽  
F. Wolter ◽  
M. Zakharyaschev
Keyword(s):  
Temporal Logic ◽  
Clear Picture ◽  
Temporal Logics ◽  
Trade Off ◽  
Spatio Temporal ◽  
Spatial Logics

In this paper, we construct and investigate a hierarchy of spatio-temporal formalisms that result from various combinations of propositional spatial and temporal logics such as the propositional temporal logic PTL, the spatial logics RCC-8, BRCC-8, S4u and their fragments. The obtained results give a clear picture of the trade-off between expressiveness and `computational realisability' within the hierarchy. We demonstrate how different combining principles as well as spatial and temporal primitives can produce NP-, PSPACE-, EXPSPACE-, 2EXPSPACE-complete, and even undecidable spatio-temporal logics out of components that are at most NP- or PSPACE-complete.

scholarly journals Using temporal logics to express search control knowledge for planning

2000 ◽  
Vol 116 (1-2) ◽  
pp. 123-191 ◽  
Author(s):  
Fahiem Bacchus ◽  
Froduald Kabanza
Keyword(s):  
Temporal Logics ◽  
Control Knowledge ◽  
Search Control

scholarly journals On the Model Checking Problem for Some Extension of CTL*

2020 ◽  
Vol 27 (4) ◽  
pp. 428-441
Author(s):  
Anton Romanovich Gnatenko ◽  
Vladimir Anatolyevich Zakharov
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Reactive Systems ◽  
Expressive Power ◽  
Binary Relations ◽  
Temporal Logics ◽  
Distinctive Features ◽  
Verification Problem ◽  
Finite State ◽  
Infinite Sequences

Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.

Planning with Spatio-Temporal Search Control Knowledge

2018 ◽  
Vol 30 (10) ◽  
pp. 1915-1928 ◽  
Author(s):  
Xu Lu ◽  
Cong Tian ◽  
Zhenhua Duan ◽  
Hongwei Du
Keyword(s):  
Spatio Temporal ◽  
Control Knowledge ◽  
Search Control ◽  
Temporal Search

scholarly journals The temporal logic of coalgebras via Galois algebras

2002 ◽  
Vol 12 (6) ◽  
pp. 875-903 ◽  
Author(s):  
BART JACOBS
Keyword(s):  
State Space ◽  
Temporal Logic ◽  
Metric Spaces ◽  
Linear Temporal Logic ◽  
The State ◽  
Temporal Logics ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Polynomial Functors

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

Sign in / Sign up

Export Citation Format

Share Document