The multi-agent Socially Friendly Coalition Logic SFCL was introduced in [1]. The present paper focuses on the two-agent fragment SFCL ( 2 ) of SFCL . We illustrate the use of SFCL ( 2 ) for formalising reasoning about two-agent interaction enabling cooperative strategic behaviour. Then we prove completeness of an axiomatic system for the 2-agent case SFCL ( 2 ) essentially extracted from the one for SFCL presented in [1] . The proof method is fully constructive and produces finite tree-like models for all consistent SFCL ( 2 ) -formulae, thus also implying decidability of that logic. The proof method is, in principle, generically extendable to the full SFCL and to various other logics for local strategic reasoning.

In the process of designing a computer system S and checking whether an abstract model ℳ of S verifies a given specification property η, one might have only a partial knowledge of the model, either because ℳ has not yet been completely defined (constructed) by the designer, or because it is not completely observable by the verifier. This leads to new verification problems, subsuming satisfiability and model checking as special cases. We state and discuss these problems in the case of LTL specifications, and develop a uniform tableau-based approach for their solutions.

Abstract We propose a general framework for modelling and formal reasoning about multi-agent systems and, in particular, multi-stage games where both quantitative and qualitative objectives and constraints are involved. Our models enrich concurrent game models with payoffs and guards on actions associated with each state of the model and propose a quantitative extension of the logic $${\textsf {ATL}}^{*}$$ ATL ∗ that enables the combination of quantitative and qualitative reasoning. We illustrate the framework with some detailed examples. Finally, we consider the model-checking problems arising in our framework and establish some general undecidability and decidability results for them.

We study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We propose a natural notion of higher-order knowledge of agents. Based on this notion, we define a class of knowledge-based strategies, and consider the problem of synthesis of strategies of this class. We introduce a multi-agent extension, MKBSC, of the well-known knowledge-based subset construction applied to such games. Its iterative applications turn out to compute higher-order knowledge of the agents. We show how the MKBSC can be used for the design of knowledge-based strategy profiles, and investigate the transfer of existence of such strategies between the original game and in the iterated applications of the MKBSC, under some natural assumptions. We also relate and compare the “intensional” view on knowledge-based strategies based on explicit knowledge representation and update, with the “extensional” view on finite memory strategies based on finite transducers and show that, in a certain sense, these are equivalent.

We introduce and study a natural extension of the Alternating time temporal logic ATL , called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called the coalitional goal assignment operator ⦉ γ ⦊, where γ is a mapping assigning to each set of players in the game its coalitional goal , formalised by a path formula of the language of TLCGA, i.e., a formula prefixed with a temporal operator X , U , or G , representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⦉ γ ⦊ intuitively says that there is a strategy profile Σ for the grand coalition Agt such that for each coalition C , the restriction Σ | C of Σ to C is a collective strategy of C that enforces the satisfaction of its objective γ (C) in all outcome plays enabled by Σ | C . We establish fixpoint characterizations of the temporal goal assignments in a μ-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy–Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.

Abstract We study the first-order theories of some natural and important classes of coloured trees, including the four classes of trees whose paths have the order type respectively of the natural numbers, the integers, the rationals, and the reals. We develop a technique for approximating a tree as a suitably coloured linear order. We then present the first-order theories of certain classes of coloured linear orders and use them, along with the approximating technique, to establish complete axiomatisations of the four classes of trees mentioned above.

We investigate repeated win-lose coordination games and analyse when and how rational players can guarantee eventual coordination in such games. Our study involves both the setting with a protocol shared in advance as well as the scenario without an agreed protocol. In both cases, we focus on the case without any communication amongst the players once the particular game to be played has been revealed to them. We identify classes of coordination games in which coordination cannot be guaranteed in a single round, but can eventually be achieved in several rounds by following suitable coordination protocols. In particular, we study coordination using protocols invariant under structural symmetries of games under some natural assumptions, such as: Priority hierarchies amongst players, different patience thresholds, use of focal groups, and gradual coordination by contact.

Abstract We develop a logic-based framework for formal specification and algorithmic verification ofhomogeneousanddynamicconcurrent multi-agent transition systems. Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. The state transitions are therefore determined only by the vector of numbers of agents performing each action and are specified symbolically, by means of conditions on these numbers definable in Presburger arithmetic. The agents are divided intocontrollable(by the system supervisor/controller) anduncontrollable, representing the environment or adversary. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a language for formal specification we use a suitably extended version of Alternating-time Temporal Logic, where one can specify properties of the type “a coalition of (at least)ncontrollable agents can ensure against (at most)muncontrollable agents that any possible evolution of the system satisfies a given objective $$\gamma$$ γ ″, where $$\gamma$$ γ is specified again as a formula of that language and each ofnandmis either a fixed number or a variable that can be quantified over. We provide formal semantics to our logic $${\mathcal {L}}_{\textsc {hdmas}}$$ LHDMAS and define normal form of its formulae. We then prove that every formula in $${\mathcal {L}}_{\textsc {hdmas}}$$ LHDMAS is equivalent in the finite to one in a normal form and develop an algorithm for global model checking of formulae in normal form in finite HDMAS models, which invokes model checking truth of Presburger formulae. We establish worst case complexity estimates for the model checking algorithm and illustrate it on a running example.

Abstract We study pure coordination games where in every outcome, all players have identical payoffs, ‘win’ or ‘lose’. We identify and discuss a range of ‘purely rational principles’ guiding the reasoning of rational players in such games and compare the classes of coordination games that can be solved by such players with no preplay communication or conventions. We observe that it is highly nontrivial to delineate a boundary between purely rational principles and other decision methods, such as conventions, for solving such coordination games.

We study the problem of minimisation of a given finite pointed Kripke model satisfying a given CTL formula, with the only objective to preserve the satisfaction of that formula in the resulting reduced model. We consider minimisations of the model with respect both to state-based redundancies and formula-based redundancies in that model. We develop a procedure computing all such minimisations, illustrate it with some examples, and provide some complexity analysis for it.

We introduce several versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game. Thus, the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators and on the meta-level, where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game. We introduce and analyze an unbounded and (ordinal) bounded GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We show that, in bounded GTS, truth of ATL formulae can always be determined in finite time, that is, without constructing infinite paths. We also introduce a nonequivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

We consider a variation of the branching time logic CTL with non-standard, "finitely bounded" semantics (FBS). FBS is naturally defined as game-theoretic semantics where the proponent of truth of an eventuality must commit to a time limit (number of transition steps) within which the formula should become true on all (resp. some) paths starting from the state where the formula is evaluated. The resulting version CTL(FB) of CTL differs essentially from the standard one as it no longer has the finite model property. We develop two tableaux systems for CTL(FB). The first one deals with infinite sets of formulae, whereas the second one deals with finite sets of formulae in a slightly extended language allowing explicit indication of time limits in formulae. We prove soundness and completeness of both systems and also show that the latter tableaux system provides an EXPTIME decision procedure for it and thus prove EXPTIME-completeness of the satisfiability problem.

We investigate the minimal length and nesting depth of temporal formulae that distinguish two given non-bisimilar finite pointed transition systems. We show that such formula can always be constructed in length at most exponential in the combined number of states of both transition systems, and give an example with exponential lower bound, for several common temporal languages. We then show that by using renamings of subformulae or explicit assignments the length of the distinguishing formula can always be reduced to one that is bounded above by a cubic polynomial on the combined size of both transition systems. This is also a bound for the size obtained by using DAG representation of formulae. We also prove that the minimal nesting depth for such formula is less than the combined size of the two state spaces and obtain some tight upper bounds.

We consider models of multi-player games where abilities of players and coalitions are defined in terms of sets of outcomes which they can effectively enforce. We extend the well-studied state effectivity models of one-step games in two different ways. On the one hand, we develop multiple state effectivity functions associated with different long-term temporal operators. On the other hand, we define and study coalitional path effectivity models where the outcomes of strategic plays are infinite paths. For both extensions we obtain representation results with respect to concrete models arising from concurrent game structures. We also apply state and path coalitional effectivity models to provide alternative, arguably more natural and elegant semantics to the alternating-time temporal logic ATL*, and discuss their technical and conceptual advantages.

We develop a sound, complete, and practically implementable tableau-based decision method for constructive satisfiability testing and model synthesis for the fragment ATL + of the full alternating-time temporal logic ALT * . The method extends in an essential way a previously developed tableau-based decision method for ATL and works in 2EXPTIME, which is the optimal worst-case complexity of the satisfiability problem for ATL + . We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL + formulas can reduce the complexity of the satisfiability problem.

This is a selective survey and discussion of some of the landmark undecidability results in temporal logic, beginning with Turing's undecidability of the Halting problem which, in retrospect, can be regarded as the historically first undecidability result for a suitable temporal logic over configuration graphs of Turing machines. I will discuss some of the natural habitats of undecidable temporal logics, such as first-order, interval-based and real time temporal logics, as well as some extensions that often lead to undecidability, such as two-dimensional temporal logics and temporal-epistemic logics.

We compare the expressiveness of the fragments of Halpern and Shoham’s interval logic (HS), i.e., of all interval logics with modal operators associated with Allen’s relations between intervals in linear orders. We establish a complete set of interdefinability equations between these modal operators, and thus obtain a complete classification of the family of 2^12 fragments of HS with respect to their expressiveness. Using that result and a computer program, we have found that there are 1347 expressively different such interval logics over the class of all linear orders.

Unlike the Moon, the dark side of interval temporal logics is the one we usually see: their ubiquitous undesirability. Identifying minimal undecidable interval logics is thus a natural and important issue in the research agenda in the area. The decidability status of a logic often depends on the class of models (in our case, the class of interval structures)in which it is interpreted. In this paper, we have identified several new minimal undecidable logics amongst the fragments of Halpern-Shoham logic HS, including the logic of the overlaps relation, over the classes of all and finite linear orders, as well as the logic of the meet and subinterval relations, over the class of dense linear orders. Together with previous undecid ability results, this work contributes to delineate the border of the dark side of interval temporal logics quite sharply.

Interval temporal logics formalize reasoning about interval structures over (usually) linearly ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is “met by” the current one and to an interval that “meets” the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the lengths of intervals. We argue that MPNL can be successfully used in different areas of artificial intelligence to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined subfragment of the two-variable fragment FO2[N, =, <, s] of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full FO2[N, =, <, s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.

In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.

Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

We investigate fragments of Halpern-Shoham's interval logic HS involving the modal operators for the relations of left or right overlap of intervals. We prove that most of these fragments are undecidable, by employing a non-trivial reduction from the octant tiling problem.

We develop an incremental tableau-based decision procedure for the alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we believe that our tableaux are 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 an incremental-tableau-based decision procedure for the multi-agent epistemic logic MAEL(CD) (aka S5_n (CD)), whose language contains operators of individual knowledge for a finite set agents of agents, as well as operators of distributed and common knowledge among all agents in agents. Our tableau procedure works in (deterministic) exponential time, thus establishing an upper bound for MAEL(cd)-satisfiability that matches the (implicit) lower-bound known from earlier results, which implies ExpTime-completeness of MAEL(CD)-satisfiability. Therefore, our procedure provides a complexity-optimal algorithm for checking MAEL(CD)-satisfiability, which, however, in most cases is much more efficient. We prove soundness and completeness of the procedure, and illustrate it with an example.

In Alternating-time Temporal Logic (ATL), one can express statements about the strategic ability of an agent (or a coalition of agents) to achieve a goal ϕ such as: "agent i can choose a strategy such that, if i follows this strategy then, no matter what other agents do, ϕ will always be true". However, strategies in ATL are revocable in the sense that in the evaluation of the goal ϕ the agent i is no longer restricted by the strategy she has chosen in order to reach the state where the goal is evaluated. In this paper we consider alternative variants of ATL where strategies, on the contrary, are irrevocable. The difference between revocable and irrevocable strategies shows up when we consider the ability to achieve a goal which, again, involves (nested) strategic ability. Furthermore, unlike in the standard semantics of ATL, memory plays an essential role in the semantics based on irrevocable strategies.

Modal formulae express monadic second-order properties on Kripke frames, but in many important cases these have first-order equivalents. Computing such equivalents is important for both logical and computational reasons. On the other hand, canonicity of modal formulae is important, too, because it implies frame-completeness of logics axiomatized with canonical formulae. Computing a first-order equivalent of a modal formula amounts to elimination of second-order quantifiers. Two algorithms have been developed for second-order quantifier elimination: SCAN, based on constraint resolution, and DLS, based on a logical equivalence established by Ackermann. In this paper we introduce a new algorithm, SQEMA, for computing first-order equivalents (using a modal version of Ackermann's lemma) and, moreover, for proving canonicity of modal formulae. Unlike SCAN and DLS, it works directly on modal formulae, thus avoiding Skolemization and the subsequent problem of unskolemization. We present the core algorithm and illustrate it with some examples. We then prove its correctness and the canonicity of all formulae on which the algorithm succeeds. We show that it succeeds not only on all Sahlqvist formulae, but also on the larger class of inductive formulae, introduced in our earlier papers. Thus, we develop a purely algorithmic approach to proving canonical completeness in modal logic and, in particular, establish one of the most general completeness results in modal logic so far.

In Conradie, Goranko, and Vakarelov (2006, Logical Methods in Computer Science, 2) we introduced a new algorithm, ⁠, for computing first-order equivalents and proving the canonicity of modal formulae of the basic modal language. Here we extend ⁠, first to arbitrary and reversive polyadic modal languages, and then to hybrid polyadic languages too. We present the algorithm, illustrate it with some examples, and prove its correctness with respect to local equivalence of the input and output formulae, its completeness with respect to the polyadic inductive formulae introduced in Goranko and Vakarelov (2001, J. Logic. Comput., 11, 737–754) and Goranko and Vakarelov (2006, Ann. Pure. Appl. Logic, 141, 180–217), and the d-persistence (with respect to descriptive frames) of the formulae on which the algorithm succeeds. These results readily expand to completeness with respect to hybrid inductive polyadic formulae and di-persistence (with respect to discrete frames) in hybrid reversive polyadic languages.

We introduce hybrid Ockhamist temporal logic, which combines the mechanisms of hybrid logic with Ockhamist semantics by employing nominals, satisfaction operators, binders, and quantifiers over branches. We provide a complete (with respect to bundled trees semantics) axiomatic system for the basic hybrid Ockhamist temporal logic (HOT) and for some of its extensions including the full hybrid Ockhamist temporal logic. The fill system is expressively equivalent to the first-order logic over trees extended with branch quantifiers which was proved decidable previously.

Building on a new approach to polyadic modal languages and Sahlqvist formulas we define Sahlqvist formulas in hybrid polyadic modal languages containing nominals and universal modality or satisfaction operators. Particularly interesting is the case of reversive polyadic languages, closed under all ‘inverses’ of polyadic modalities because the minimal valuations arising in the computation of the first‐order equivalents of polyadic Sahlqvist formulae are definable in such languages and that makes the proof of first‐order definability and canonicity of these formulas a simple syntactic exercise. Furthermore, the first‐order definability of Sahlqvist formulas immediately transfers to arbitrary polyadic languages, while the direct transfer of canonicity requires a more involved proof‐theoretic analysis.

We propose a generalization of Sahlqvist formulae to polyadic modal languages by representing modal polyadic languages in a combinatorial style and thus, in particular, developing what we believe to be the right approach to Sahlqvist formulae at all. The class of polyadic Sahlqvist formulae PSF defined here expands essentially the so far known one. We prove first-order definability and canonicity for the class PSF.

The paper investigates a simple and natural enrichment of the usual modal language ℒ = ℒ(□) with an auxiliary ‘universal’ modality u⃞ having Kripke semantics: u⃞ϕ is true at a world of a model iff Φ is valid in the model The enriched language ℒu⃞ = ℒ(□,⃞) turns out to be fairly different from the classical one. In particular the notions of satisfiability, validity and consequence in models become interreducible. Section 2 is devoted to modal definability in ℒu⃞. Model-theoretic characterizations of this definability are obtained. ℒu⃞-definability is proved to be equivalent with sequential definability in Lintroduced by Kapron. In section 3 the minimal normal ℒu⃞-logic Ku⃞ is axiomatized and a general model-completeness theroem for the family of normal extensions of Ku⃞ is proved. Section 4 deals with minimal extensions ℒu⃞ logics axiomatized with schemata of ℒ over Ku⃞. A general study to transfer of properties of ℒ-logics to their minimal extensions is initiated. Transfer of incompleteness, strong completeness, compactness and filtration is proved. The problems of transferring completeness, finite completeness and decidabilit are investigated and several general results are obtained. Uniform reductions of these properties of ℒu⃞-logics to corresponding natural properties in thier classical fragments are established. For a large class of ℒ-logics, completeness is shown to be inherited in thier minimal extensions. However, the general transferring problems remain still open.In section 5 several concrete completeness and decidability results for logics with essentially ℒu⃞-axiomatics are stated and some other applications of u⃞ are sketched. In an appendix independent join of ℒu⃞-logics is introduced and proved to preserve completeness when applied to minimal extensions. Besides the technical results, the paper pursues two main purposes: first, to advertise the universal modality as a natural and helpful tool, providing a better medium for the mission of modality; and second, to illustrate the typical problems arising when enrichments of modal languages are investigated.