We develop an incremental tableau-based decision procedures for the
Alternating-time temporal logic ATL and some of its variants.
While running within the theoretically established complexity upper bound, we claim that our tableau is practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure.
We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau procedure runs in exponential time, matching the lower bound obtained by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal decision procedure for CMATEL(CD+LT).
Priest has provided a simple tableau calculus for Chellas's conditional logic Ck. We provide rules which, when added to Priest's system, result in tableau calculi for Chellas's CK and Lewis's VC. Completeness of these tableaux, however, relies on the cut rule.
The paper provides a tableau approach to definite descriptions. We focus on several formalizations of the so-called minimal free description theory (MFD) usually formulated axiomatically in the setting of free logic. We consider five analytic tableau systems corresponding to different kinds of free logic, including the logic of definedness applied in computer science and constructive mathematics for dealing with partial functions (here called negative quasi-free logic). The tableau systems formalise MFD based on PFL (positive free logic), NFL (negative free logic), PQFL and NQFL (the quasi-fre…
A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of…
命题线性时态逻辑（Propositional Linear Time Temporal Logic，LTL）是一种面向计算应用的标准时态逻辑，许多推理技术和工具已经被开发出来。然而，这种逻辑的tableaux看起来不像传统的树形tableau系统，它们的处理通常非常复杂。我们提出了一个新的简单的传统风格的树形画面LTL，并证明它是健全的和完整的。除了易于理解，向学生介绍和手动使用外，它似乎也易于实现，并有望在自动化方面具有竞争力。它特别适合于并行实现。
命题线性时态逻辑（Propositional Linear Time Temporal Logic，LTL）是一种面向计算应用的标准时态逻辑，许多推理技术和工具已经被开发出来。然而，这种逻辑的tableaux看起来不像传统的树形tableau系统，它们的处理通常非常复杂。在本文中，我们介绍了一种新的风格的tableau规则，支持一个新的简单的传统风格的树形tableau LTL。我们证明它是健全和完整的。除了易于理解，向学生介绍和使用外，它还易于实现，并且与最先进的系统相比具有竞争力。它特别适合于并行实现。
This paper describes a method for converting formulas in finite propositional linear-time temporal logic (Finite LTL) into finite-state automata whose languages are the models of the given formula. Finite LTL differs from traditional LTL in that formulas are interpreted with respect to finite, rather than infinite, sequences of states; this fact means that traditional finite-state automata, rather than ω-automata such as those developed by Büchi and others, suffice for recognizing models of such formulas. The approach considered is based on well-known tableau-construction techniques developed …
In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time temporal logic, with an EXPSPACE-complete satisfiability problem, which has been successfully applied to the verification of real-time systems. In contrast to LTL, adding past operators to TPTL makes the satisfiability problem for the resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass and tree-shaped tableau for both TPTL and bounded TPTL…
We present a first result towards the use of entailment in- side relational dual tableau-based decision procedures. To this end, we introduce a fragment of RL(1) which admits a restricted form of composition, (R ; S) or (R ; 1), where the left subterm R of (R ; S) is only allowed to be either the constant 1, or a Boolean term neither containing the complement operator nor the constant 1, while in the case of (R ; 1), R can only be a Boolean term involving relational variables and the operators of intersection and of union. We prove the decidability of the fragment by defining a dual tableau- b…
Sentential Calculus with Identity (SCI) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of SCI-formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision proc…
We propose a model checking algorithm to test properties of systems that are expressed in the multi-agent temporal logic ATL+. The specificities of this algorithm are: it is on-the-fly, generating states only when they are needed, and it works by constructing a candidate formal proof in an inference system inspired by tableau proof systems.
This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the mu-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce a terminating tableau system for the logics we study, based on Kozen's tableau for the mu-calculus, and the one of Fitting and Massacci for modal logic.
Stockholm University（斯德哥尔摩大学）；The John Paul II Catholic University of Lublin（卢布林若望保禄二世天主教大学）
We consider systems of rational agents who act and interact in pursuit of their individual and collective objectives. We study and formalise the reasoning of an agent, or of an external observer, about the expected choices of action of the other agents based on their objectives, in order to assess the reasoner's ability, or expectation, to achieve their own objective. To formalize such reasoning we extend Pauly's Coalition Logic with three new modal operators of conditional strategic reasoning, thus introducing the Logic for Local Conditional Strategic Reasoning ConStR. We provide formal seman…
Temporal logics are extensively used for the specification of on-going behaviours of reactive systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviours in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalise concepts such as certainty or quality. We introduce and study FSL---a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics descr…
STIT (sees to it that) semantics is one of the most prominent tools in modal logic of agency, widely used among both philosophers and responsible AI scholars. STIT logic surveys the properties of agents seeing to it that some state of affairs holds without specifying concrete actions by which that state of affairs is guaranteed. In comparison with other multi-agent modal logics, the main advantage of STIT theories is expressive power. STIT logic allows to study not only statements about agents abilities to perform certain actions (as it is in variations of Coalition Logic or Propositional Dyna…
Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties where the individual computation paths are chosen by the strategic choices of a coalition of agents in a multi-agent system. We introduce HyperATL*, an extension of computation tree logic with path variables and strategy quantifiers. HyperATL* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid inform…
