scholarly journals Propositional Dynamic Logic for Planning

2020 ◽  
Author(s):  
Mario Folhadela Benevides ◽  
Anna Moreira De Oliveira
Keyword(s):  
Computational Complexity ◽  
Dynamic Logic ◽  
Planning Problem ◽  
Propositional Dynamic Logic ◽  
Reasoning About Actions ◽  
Future Work ◽  
New Framework

This paper presents an on going work on Propositional Dynamic Logic PDL in which atomic programs are STRIPS actions. We think that this new framework is appropriate to reasoning about actions and plans when dealing with planning problem. Unlike, PDL atomic programs, STRIPS actions have pre-conditions and post-conditions. We propose a novel operator of action composition that takes in account the features of STRIPS actions. We propose an axiomatization and prove its soundness. Completeness, decidability and computational complexity are left as future work.

Decidability and Complexity of Some Finitely-valued Dynamic Logics

2021 ◽  
Author(s):  
Igor Sedlár
Keyword(s):  
Transitive Closure ◽  
Description Logics ◽  
Dynamic Logic ◽  
Time Algorithm ◽  
Action Execution ◽  
Propositional Dynamic Logic ◽  
Relational Models ◽  
Reasoning About Actions ◽  
Decidability And Complexity ◽  
Dynamic Logics

Propositional Dynamic Logic, PDL, is a well known modal logic formalizing reasoning about complex actions. We study many-valued generalizations of PDL based on relational models where satisfaction of formulas in states and accessibility between states via action execution are both seen as graded notions, evaluated in a finite Łukasiewicz chain. For each n>1, the logic PDŁn is obtained using the n-element Łukasiewicz chain, PDL being equivalent to PDŁ2. These finitely-valued dynamic logics can be applied in formalizing reasoning about actions specified by graded predicates, reasoning about costs of actions, and as a framework for certain graded description logics with transitive closure of roles. Generalizing techniques used in the case of PDL we obtain completeness and decidability results for all PDŁn. A generalization of Pratt's exponential-time algorithm for checking validity of formulas is given and EXPTIME-hardness of each PDŁn validity problem is established by embedding PDL into PDŁn.

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.

scholarly journals Dynamic Linear Time Temporal Logic

1997 ◽  
Vol 4 (8) ◽  
Author(s):  
Jesper G. Henriksen ◽  
P. S. Thiagarajan
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Order Theory ◽  
Simple Extension ◽  
Propositional Dynamic Logic ◽  
First Order ◽  
Time Semantics ◽  
Linear Time Temporal Logic ◽  
Obvious Manner

A simple extension of the propositional temporal logic of linear<br />time is proposed. The extension consists of strengthening the until<br />operator by indexing it with the regular programs of propositional<br />dynamic logic (PDL). It is shown that DLTL, the resulting logic, is<br />expressively equivalent to S1S, the monadic second-order theory<br />of omega-sequences. In fact a sublogic of DLTL which corresponds<br />to propositional dynamic logic with a linear time semantics is<br />already as expressive as S1S. We pin down in an obvious manner<br />the sublogic of DLTL which correponds to the first order fragment<br />of S1S. We show that DLTL has an exponential time decision<br />procedure. We also obtain an axiomatization of DLTL. Finally,<br />we point to some natural extensions of the approach presented<br />here for bringing together propositional dynamic and temporal<br />logics in a linear time setting.

Chapter 34. Stochastic Boolean Satisfiability

2021 ◽  
Author(s):  
Stephen M. Majercik
Keyword(s):  
Artificial Intelligence ◽  
Computational Complexity ◽  
Probabilistic Reasoning ◽  
Broad Class ◽  
Theoretical Perspective ◽  
Boolean Satisfiability ◽  
Probabilistic Planning ◽  
Empirical Results ◽  
Future Work ◽  
Planning Problems

Stochastic satisfiability (SSAT) is an extension of satisfiability (SAT) that merges two important areas of artificial intelligence: logic and probabilistic reasoning. Initially suggested by Papadimitriou, who called it a “game against nature”, SSAT is interesting both from a theoretical perspective–it is complete for PSPACE, an important complexity class–and from a practical perspective–a broad class of probabilistic planning problems can be encoded and solved as SSAT instances. This chapter describes SSAT and its variants, their computational complexity, applications of SSAT, analytical results, algorithms and empirical results, related work, and directions for future work.

Sign in / Sign up

Export Citation Format

Share Document