-
Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is $Σ^1_1$-hard
Authors:
Rustam Galimullin,
Louwe B. Kuijer
Abstract:
Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an extension of Public Announcement Logic with common knowledge modality and quantifiers over announcements. We show that the satisfiability problem of APALC on S5-models, as well as that of two other related logics with quantification and common knowledge, is $Σ^1_1$-hard. This implies that neither the validities nor the satisfi…
▽ More
Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an extension of Public Announcement Logic with common knowledge modality and quantifiers over announcements. We show that the satisfiability problem of APALC on S5-models, as well as that of two other related logics with quantification and common knowledge, is $Σ^1_1$-hard. This implies that neither the validities nor the satisfiable formulas of APALC are recursively enumerable. Which, in turn, implies that APALC is not finitely axiomatisable.
△ Less
Submitted 11 July, 2023;
originally announced July 2023.
-
Simple Axioms for Local Properties
Authors:
Philippe Balbiani,
Wiebe van der Hoek,
Louwe B. Kuijer
Abstract:
Correspondence theory allows us to create sound and complete axiomatizations for modal logic on frames with certain properties. For example, if we restrict ourselves to transitive frames we should add the axiom $\square φ\rightarrow \square\squareφ$ which, among other things, can be interpreted as positive introspection. One limitation of this technique is that the frame property and the axiom are…
▽ More
Correspondence theory allows us to create sound and complete axiomatizations for modal logic on frames with certain properties. For example, if we restrict ourselves to transitive frames we should add the axiom $\square φ\rightarrow \square\squareφ$ which, among other things, can be interpreted as positive introspection. One limitation of this technique is that the frame property and the axiom are assumed to hold globally, i.e., the relation is transitive throughout the frame, and the agent's knowledge satisfies positive introspection in every world.
In a modal logic with local properties, we can reason about properties that are not global. So, for example, transitivity might hold only in certain parts of the model and, as a result, the agent's knowledge might satisfy positive introspection in some worlds but not in others. Van Ditmarsch et al. (2012) introduced sound and complete axiomatizations for modal logics with certain local properties. Unfortunately, those axiomatizations are rather complex. Here, we introduce far simpler axiomatizations for a wide range of local properties.
△ Less
Submitted 11 July, 2023;
originally announced July 2023.
-
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL* is Even Harder
Authors:
Marie Fortin,
Louwe B. Kuijer,
Patrick Totzke,
Martin Zimmermann
Abstract:
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics.
In this paper we settle the exact…
▽ More
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics.
In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_1^2$-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We also prove this bound to be tight. Furthermore, we prove that both countable and finitely-branching satisfiability for HyperCTL* are as hard as truth in second-order arithmetic, i.e. still highly undecidable.
Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $Π_1^1$-complete.
△ Less
Submitted 30 March, 2023; v1 submitted 29 March, 2023;
originally announced March 2023.
-
HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL* Satisfiability is $Σ_1^2$-complete
Authors:
Marie Fortin,
Louwe B. Kuijer,
Patrick Totzke,
Martin Zimmermann
Abstract:
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics.
In this paper we settle the exact…
▽ More
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics.
In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_1^2$-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is $Π_1^1$-complete.
△ Less
Submitted 10 May, 2021;
originally announced May 2021.
-
Strengthening Gossip Protocols using Protocol-Dependent Knowledge
Authors:
Hans van Ditmarsch,
Malvin Gattinger,
Louwe B. Kuijer,
Pere Pardo
Abstract:
Distributed dynamic gossip is a generalization of the classic telephone problem in which agents communicate to share secrets, with the additional twist that also telephone numbers are exchanged to determine who can call whom. Recent work focused on the success conditions of simple protocols such as "Learn New Secrets" (LNS) wherein an agent a may only call another agent b if a does not know b's se…
▽ More
Distributed dynamic gossip is a generalization of the classic telephone problem in which agents communicate to share secrets, with the additional twist that also telephone numbers are exchanged to determine who can call whom. Recent work focused on the success conditions of simple protocols such as "Learn New Secrets" (LNS) wherein an agent a may only call another agent b if a does not know b's secret. A protocol execution is successful if all agents get to know all secrets. On partial networks these protocols sometimes fail because they ignore information available to the agents that would allow for better coordination. We study how epistemic protocols for dynamic gossip can be strengthened, using epistemic logic as a simple protocol language with a new operator for protocol-dependent knowledge. We provide definitions of different strengthenings and show that they perform better than LNS, but we also prove that there is no strengthening of LNS that always terminates successfully. Together, this gives us a better picture of when and how epistemic coordination can help in the dynamic gossip problem in particular and distributed systems in general.
△ Less
Submitted 29 July, 2019;
originally announced July 2019.
-
Arrow Update Synthesis
Authors:
Hans van Ditmarsch,
Wiebe van der Hoek,
Barteld Kooi,
Louwe B. Kuijer
Abstract:
In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a…
▽ More
In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a modality for quantification over arrow update models. Arrow update models are an alternative to the well-known action models. We provide an axiomatization of AAUML. The axiomatization is a rewrite system allowing to eliminate arrow update modalities from any given formula, while preserving truth. Thus, AAUML is decidable and equally expressive as the base multi-agent modal logic. Our main result is to establish arrow update synthesis: if there is an arrow update model after which phi, we can construct (synthesize) that model from phi. We also point out some pregnant differences in update expressivity between arrow update logics, action model logics, and refinement modal logic.
△ Less
Submitted 24 October, 2019; v1 submitted 3 February, 2018;
originally announced February 2018.
-
Arbitrary Arrow Update Logic with Common Knowledge is neither RE nor co-RE
Authors:
Louwe B. Kuijer
Abstract:
Arbitrary Arrow Update Logic with Common Knowledge (AAULC) is a dynamic epistemic logic with (i) an arrow update operator, which represents a particular type of information change and (ii) an arbitrary arrow update operator, which quantifies over arrow updates.
By encoding the execution of a Turing machine in AAULC, we show that neither the valid formulas nor the satisfiable formulas of AAULC ar…
▽ More
Arbitrary Arrow Update Logic with Common Knowledge (AAULC) is a dynamic epistemic logic with (i) an arrow update operator, which represents a particular type of information change and (ii) an arbitrary arrow update operator, which quantifies over arrow updates.
By encoding the execution of a Turing machine in AAULC, we show that neither the valid formulas nor the satisfiable formulas of AAULC are recursively enumerable. In particular, it follows that AAULC does not have a recursive axiomatization.
△ Less
Submitted 27 July, 2017;
originally announced July 2017.
-
The Undecidability of Arbitrary Arrow Update Logic
Authors:
Hans van Ditmarsch,
Wiebe van der Hoek,
Louwe B. Kuijer
Abstract:
Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefo…
▽ More
Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable, by a reduction of the tiling problem.
△ Less
Submitted 19 September, 2016;
originally announced September 2016.
