Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as Alternating-time Temporal Logic (ATL). The key insight (...) in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as group can cooperate to bring about iff it is common knowledge in that . The resulting logic — Alternating-time Temporal Epistemic Logic (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems. (shrink)

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be (...) captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances . Due to its greater expressive power, this logic turns out to behave quite differently from both and conditional logics. We provide finite axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line is not recursively enumerable. This result is proved by an encoding of Diophantine equations. (shrink)

The article studies knowledge in multiagent systems where data available to the agents may have small errors. To reason about such uncertain knowledge, a formal semantics is introduced in which indistinguishability relations, commonly used in the semantics for epistemic logic S5, are replaced with metrics to capture how much two epistemic worlds are different from an agent’s point of view. The main result is a logical system sound and complete with respect to the proposed semantics.

In [STU 00, KUT 03] we introduced a family of ‘modal' languages intended for talking about distances. These languages are interpreted in ‘distance spaces' which satisfy some of the standard axioms of metric spaces. Among other things, we singled out decidable logics of distance spaces and proved expressive completeness results relating classical and modal languages. The aim of this paper is to axiomatize the modal fragments of the semantically defined distance logics of [KUT 03] and give a new proof of (...) their decidability. (shrink)

We propose a non-standard interpretation of Alternating-time Temporal Logic with imperfect information, for which no commonly accepted semantics has been proposed yet. Rather than changing the semantic structures, we generalize the usual interpretation of formulae in single states to sets of states. We also propose a new epistemic operator for ?practical? or ?constructive? knowledge, and we show that the new logic (which we call Constructive Strategic Logic) is strictly more expressive than most existing solutions, while it retains the same model (...) checking complexity. Finally, we study properties of constructive knowledge and other operators in this non-standard semantics. (shrink)

We discuss games of both perfect and imperfect information at two levels of structural detail: players’ local actions, and their global powers for determining outcomes of the game. We propose matching logical languages for both. In particular, at the ‘action level’, imperfect information games naturally model a combined ‘dynamic-epistemic language’ – and we find correspondences between special axioms and particular modes of playing games with their information dynamics. At the ‘outcome level’, we present suitable notions of game equivalence, plus some (...) simple representation results. (shrink)