An infinitary encoding of temporal equilibrium logic

2015 ◽  
Vol 15 (4-5) ◽  
pp. 666-680 ◽  
Author(s):  
PEDRO CABALAR ◽  
MARTÍN DIÉGUEZ ◽  
CONCEPCIÓN VIDAL
Keyword(s):  
Logic Programming ◽  
Temporal Logic ◽  
Linear Time ◽  
Answer Set Programming ◽  
Modal Operators ◽  
Temporal Logic Programming ◽  
Linear Time Temporal Logic ◽  
Answer Set

AbstractThis paper studies the relation between two recent extensions of propositional Equilibrium Logic, a well-known logical characterisation of Answer Set Programming. In particular, we show how Temporal Equilibrium Logic, which introduces modal operators as those typically handled in Linear-Time Temporal Logic (LTL), can be encoded into Infinitary Equilibrium Logic, a recent formalisation that allows the use of infinite conjunctions and disjunctions. We prove the correctness of this encoding and, as an application, we further use it to show that the semantics of the temporal logic programming formalism called TEMPLOG is subsumed by Temporal Equilibrium Logic.

scholarly journals Linear-Time Temporal Answer Set Programming

2021 ◽  
pp. 1-55
Author(s):  
FELICIDAD AGUADO ◽  
PEDRO CABALAR ◽  
MARTÍN DIÉGUEZ ◽  
GILBERTO PÉREZ ◽  
TORSTEN SCHAUB ◽  
...  
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Selection Criterion ◽  
Answer Set Programming ◽  
Logic Programs ◽  
Modal Operators ◽  
Linear Time Temporal Logic ◽  
Stable Models ◽  
Answer Set

Abstract In this survey, we present an overview on (Modal) Temporal Logic Programming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium Logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.

scholarly journals Temporal logic programs with variables

2016 ◽  
Vol 17 (2) ◽  
pp. 226-243 ◽  
Author(s):  
FELICIDAD AGUADO ◽  
PEDRO CABALAR ◽  
GILBERTO PÉREZ ◽  
CONCEPCIÓN VIDAL ◽  
MARTÍN DIÉGUEZ
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Logic Program ◽  
Answer Set Programming ◽  
Logic Programs ◽  
First Order ◽  
Linear Time Temporal Logic ◽  
Definition Of ◽  
Stable Models ◽  
Answer Set

AbstractIn this note, we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic, an extension of Answer Set Programming for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of Temporal Equilibrium Logic that shares the syntax of first-order Linear-time Temporal Logic but has different semantics, selecting some Linear-time Temporal Logic models we call temporal stable models. Then, we consider a subclass of theories (called splittable temporal logic programs) that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of safe variables that suffices to show the property of domain independence – that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard Answer Set Programming grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

scholarly journals Reasoning about actions with Temporal Answer Sets

2012 ◽  
Vol 13 (2) ◽  
pp. 201-225 ◽  
Author(s):  
LAURA GIORDANO ◽  
ALBERTO MARTELLI ◽  
DANIELE THESEIDER DUPRÉ
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Bounded Model Checking ◽  
Propositional Dynamic Logic ◽  
Reasoning About Actions ◽  
Action Language ◽  
Linear Time Temporal Logic ◽  
Answer Sets ◽  
Answer Set

AbstractIn this paper, we combine Answer Set Programming (ASP) with Dynamic Linear Time Temporal Logic (DLTL) to define a temporal logic programming language for reasoning about complex actions and infinite computations. DLTL extends propositional temporal logic of linear time with regular programs of propositional dynamic logic, which are used for indexing temporal modalities. The action language allows general DLTL formulas to be included in domain descriptions to constrain the space of possible extensions. We introduce a notion of Temporal Answer Set for domain descriptions, based on the usual notion of Answer Set. Also, we provide a translation of domain descriptions into standard ASP and use Bounded Model Checking (BMC) techniques for the verification of DLTL constraints.

Verifying linear time temporal logic properties of concurrent Ada programs with quasar

2004 ◽  
Vol XXIV (1) ◽  
pp. 17-24 ◽  
Author(s):  
S. Evangelista ◽  
C. Kaiser ◽  
J. F. Pradat-Peyre ◽  
P. Rousseau
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Linear Time Temporal Logic

Vehicle route-sequence planning using temporal logic

2002 ◽  
Vol 16 (1) ◽  
pp. 31-38
Author(s):  
KIAM TIAN SEOW ◽  
MICHEL PASQUIER
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Simple Procedure ◽  
Precedence Constraints ◽  
Sequence Planning ◽  
Vehicle Route ◽  
Passenger Travel ◽  
State Formula ◽  
Linear Time Temporal Logic ◽  
Service Task

This paper proposes a new logical framework for vehicle route-sequence planning of passenger travel requests. Each request is a fetch-and-send service task associated with two request-locations, namely, a source and a destination. The proposed framework is developed using propositional linear time temporal logic of Manna and Pnueli. The novelty lies in the use of the formal language for both the specification and theorem-proving analysis of precedence constraints among the location visits that are inherent in route sequences. In the framework, legal route sequences—each of which visits every request location once and only once in the precedence order of fetch-and-send associated with every such request—is formalized and justified, forming a basis upon which the link between a basic precedence constraint and the corresponding canonical forbidden-state formula is formally established. Over a given base route plan, a simple procedure to generate a feasible subplan based on a specification of the forbidden-state canonical form is also given. An example demonstrates how temporal logic analysis and the proposed procedure can be applied to select a final (feasible) subplan based on additional precedence constraints.

Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC)

2003 ◽  
Vol 45 (4) ◽  
Author(s):  
Daniel Große ◽  
Rolf Drechsler
Keyword(s):  
Formal Verification ◽  
Temporal Logic ◽  
Linear Time ◽  
Linear Time Temporal Logic

ZusammenfassungDer vorgestellte Ansatz ermöglicht es, für SystemC-Schaltkreisbeschreibungen, die über einer gegebenen Gatterbibliothek definiert sind, Eigenschaften zu beweisen (engl. property checking). Als Spezifikationssprache wird LTL (linear time temporal logic) verwendet. Für den Beweis einer LTL-Eigenschaft kann die Erfüllbarkeit einer Booleschen Funktion betrachtet werden, die aus der Eigenschaft und der Schaltkreisbeschreibung mittels symbolischer Methoden konstruiert wird. Im Gegensatz zu simulationsbasierten Ansätzen kann dabei Vollständigkeit gewährleistet werden. Anhand einer Fallstudie eines skalierbaren Arbiters wird die Effizienz des Beweisverfahrens untersucht.

scholarly journals Meta-Interpretive Learning Using HEX-Programs

2019 ◽  
Author(s):  
Tobias Kaminski ◽  
Thomas Eiter ◽  
Katsumi Inoue
Keyword(s):  
Logic Programming ◽  
Inductive Logic Programming ◽  
Inductive Logic ◽  
Answer Set Programming ◽  
Search Space ◽  
Recent Approach ◽  
Performance Gains ◽  
Pruning Techniques ◽  
Answer Set

Meta-Interpretive Learning (MIL) is a recent approach for Inductive Logic Programming (ILP) implemented in Prolog. Alternatively, MIL-problems can be solved by using Answer Set Programming (ASP), which may result in performance gains due to efficient conflict propagation. However, a straightforward MIL-encoding results in a huge size of the ground program and search space. To address these challenges, we encode MIL in the HEX-extension of ASP, which mitigates grounding issues, and we develop novel pruning techniques.

scholarly journals Verifying Fault-Tolerance in Probabilistic Swarm Systems

2020 ◽  
Author(s):  
Alessio Lomuscio ◽  
Edoardo Pirovano
Keyword(s):  
Fault Tolerance ◽  
Temporal Logic ◽  
Decision Problem ◽  
Swarm Robotics ◽  
Linear Time ◽  
Experimental Results ◽  
Robotic Swarms ◽  
Linear Time Temporal Logic ◽  
Probabilistic Nature

We present a method for reasoning about fault-tolerance in unbounded robotic swarms. We introduce a novel semantics that accounts for the probabilistic nature of both the swarm and possible malfunctions, as well as the unbounded nature of swarm systems. We define and interpret a variant of probabilistic linear-time temporal logic on the resulting executions, including those arising from faulty behaviour by some of the agents in the swarm. We specify the decision problem of parameterised fault-tolerance, which concerns determining whether a probabilistic specification holds under possibly faulty behaviour. We outline a verification procedure that we implement and use to study a foraging protocol from swarm robotics, and report the experimental results obtained.

Sign in / Sign up

Export Citation Format

Share Document