The Influence of the Test Operator on the Expressive Power of PDL-like Logics

2019 ◽  
Vol 29 (8) ◽  
pp. 1289-1310
Author(s):  
Linh Anh Nguyen
Keyword(s):  
Description Logics ◽  
Dynamic Logic ◽  
Expressive Power ◽  
Propositional Dynamic Logic ◽  
Test Operator ◽  
Local Reflexivity ◽  
Horn Fragment ◽  
Logical Formalism

Abstract Berman and Paterson proved that test-free propositional dynamic logic (PDL) is weaker than PDL. One would raise questions: does a similar result also hold for extensions of PDL? For example, is test-free converse-PDL (CPDL) weaker than CPDL? In what circumstances the test operator can be eliminated without reducing the expressive power of a PDL-based logical formalism? These problems have not yet been studied. As the description logics $\mathcal{ALC}_{trans}$ and $\mathcal{ALC}_{reg}$ are, respectively, variants of test-free PDL and PDL, there is a concept of $\mathcal{ALC}_{reg}$ that is not equivalent to any concept of $\mathcal{ALC}_{trans}$. Generalizing this, we prove that there is a concept of $\mathcal{ALC}_{reg}$ that is not equivalent to any concept of the logic that extends $\mathcal{ALC}_{trans}$ with inverse roles, nominals, qualified number restrictions, the universal role and local reflexivity of roles. We also provide some results for the case with RBoxes and TBoxes. One of them states that tests can be eliminated from TBoxes of the deterministic Horn fragment of $\mathcal{ALC}_{reg}$.

2-Exp Time lower bounds for propositional dynamic logics with intersection

2005 ◽  
Vol 70 (4) ◽  
pp. 1072-1086 ◽  
Author(s):  
Martin Lange ◽  
Carsten Lutz
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Open Problem ◽  
Dynamic Logic ◽  
Propositional Dynamic Logic ◽  
Tree Structures ◽  
Exponential Time ◽  
Double Exponential ◽  
Test Operator ◽  
Dynamic Logics

AbstractIn 1984. Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidabie in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004. the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime. thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.

scholarly journals A layered rule-based architecture for approximate knowledge fusion?

2010 ◽  
Vol 7 (3) ◽  
pp. 617-642 ◽  
Author(s):  
Barbara Dunin-Kęplicz ◽  
Anh Nguyen ◽  
Andrzej Szałas
Keyword(s):  
Real World ◽  
Description Logics ◽  
Dynamic Logic ◽  
Deductive Database ◽  
General Mechanism ◽  
Multi Agent Systems ◽  
Propositional Dynamic Logic ◽  
Real World Data ◽  
Knowledge Fusion ◽  
Database Technology

In this paper we present a framework for fusing approximate knowledge obtained from various distributed, heterogenous knowledge sources. This issue is substantial in modeling multi-agent systems, where a group of loosely coupled heterogeneous agents cooperate in achieving a common goal. In paper [5] we have focused on defining general mechanism for knowledge fusion. Next, the techniques ensuring tractability of fusing knowledge expressed as a Horn subset of propositional dynamic logic were developed in [13,16]. Propositional logics may seem too weak to be useful in real-world applications. On the other hand, propositional languages may be viewed as sublanguages of first-order logics which serve as a natural tool to define concepts in the spirit of description logics [2]. These notions may be further used to define various ontologies, like e.g. those applicable in the Semantic Web. Taking this step, we propose a framework, in which our Horn subset of dynamic logic is combined with deductive database technology. This synthesis is formally implemented in the framework of HSPDL architecture. The resulting knowledge fusion rules are naturally applicable to real-world data.

A stochastic interpretation of propositional dynamic logic: expressivity

2012 ◽  
Vol 77 (2) ◽  
pp. 687-716 ◽  
Author(s):  
Ernst-Erich Doberkat
Keyword(s):  
Dynamic Logic ◽  
Propositional Dynamic Logic ◽  
Adequate Treatment ◽  
Polish Spaces ◽  
Behavioral Equivalence ◽  
Straight Line ◽  
Test Operator ◽  
Model Completion ◽  
Descriptive Set ◽  
Straight Line Programs

AbstractWe propose a probabilistic interpretation of Propositional Dynamic Logic (PDL). We show that logical and behavioral equivalence are equivalent over general measurable spaces. This is done first for the fragment of straight line programs and then extended to cater for the nondeterministic nature of choice and iteration, expanded to PDL as a whole. Bisimilarity is also discussed and shown to be equivalent to logical and behavioral equivalence, provided the base spaces are Polish spaces. We adapt techniques from coalgebraic stochastic logic and point out some connections to Souslin's operation from descriptive set theory. This leads to a discussion of complete stochastic Kripke models and model completion, which permits an adequate treatment of the test operator.

scholarly journals Temporal Logics Beyond Regularity

2007 ◽  
Vol 14 (13) ◽  
Author(s):  
Martin Lange
Keyword(s):  
Model Checking ◽  
Dynamic Logic ◽  
Expressive Power ◽  
Turing Machines ◽  
Temporal Logics ◽  
Propositional Dynamic Logic ◽  
Program Correctness ◽  
Recursive Procedures ◽  
Language Classes ◽  
Context Free

Non-regular program correctness properties play an important role in the specification of unbounded buffers, recursive procedures, etc. This thesis surveys results about the relative expressive power and complexity of temporal logics which are capable of defining non-regular properties. In particular, it features Propositional Dynamic Logic of Context-Free Programs, Fixpoint Logic with Chop, the Modal Iteration Calculus, and Higher-Order Fixpoint Logic.<br /> <br />Regarding expressive power we consider two classes of structures: arbitrary transition systems as well as finite words as a subclass of the former. The latter is meant to give an intuitive account of the logics' expressive powers by relating them to known language classes defined in terms of grammars or Turing Machines. <br /> <br /> Regarding the computational complexity of temporal logics beyond regularity we focus on their model checking problems since their satisfiability problems are all highly undecidable. Their model checking complexities range between polynomial time and non-elementary.

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 Unifying Class-Based Representation Formalisms

1999 ◽  
Vol 11 ◽  
pp. 199-240 ◽  
Author(s):  
D. Calvanese ◽  
M. Lenzerini ◽  
D. Nardi
Keyword(s):  
Knowledge Representation ◽  
Description Logic ◽  
Description Logics ◽  
Expressive Power ◽  
Finite Model ◽  
Functional Dependencies ◽  
Semantic Data ◽  
Representation Systems ◽  
Frame Systems ◽  
Essential Set

The notion of class is ubiquitous in computer science and is central in many formalisms for the representation of structured knowledge used both in knowledge representation and in databases. In this paper we study the basic issues underlying such representation formalisms and single out both their common characteristics and their distinguishing features. Such investigation leads us to propose a unifying framework in which we are able to capture the fundamental aspects of several representation languages used in different contexts. The proposed formalism is expressed in the style of description logics, which have been introduced in knowledge representation as a means to provide a semantically well-founded basis for the structural aspects of knowledge representation systems. The description logic considered in this paper is a subset of first order logic with nice computational characteristics. It is quite expressive and features a novel combination of constructs that has not been studied before. The distinguishing constructs are number restrictions, which generalize existence and functional dependencies, inverse roles, which allow one to refer to the inverse of a relationship, and possibly cyclic assertions, which are necessary for capturing real world domains. We are able to show that it is precisely such combination of constructs that makes our logic powerful enough to model the essential set of features for defining class structures that are common to frame systems, object-oriented database languages, and semantic data models. As a consequence of the established correspondences, several significant extensions of each of the above formalisms become available. The high expressiveness of the logic we propose and the need for capturing the reasoning in different contexts forces us to distinguish between unrestricted and finite model reasoning. A notable feature of our proposal is that reasoning in both cases is decidable. We argue that, by virtue of the high expressive power and of the associated reasoning capabilities on both unrestricted and finite models, our logic provides a common core for class-based representation formalisms.

Sign in / Sign up

Export Citation Format

Share Document