Model checking is one of the most powerful and widespread tools for system verification with applications in many areas of computer science and artificial intelligence. The large majority of model checkers deal with properties expressed in point-based temporal logics, such as LTL and CTL. However, there exist relevant properties of systems which are inherently interval-based. Model checking algorithms for interval temporal logics (ITLs) have recently been proposed to check interval properties of computations. As the model checking problem for full Halpern and Shoham's ITL (HS for short) turns out to be decidable, but computationally heavy, research has focused on its well-behaved fragments. In this paper, we provide an almost final picture of the computational complexity of model checking for HS fragments with modalities for (a subset of) Allen's relations meets , met by , starts , and ends .

In this paper we study verification of situation calculus action theories against first-order mu-calculus with quantification across situations. Specifically, we consider mu-La and mu-Lp, the two variants of mu-calculus introduced in the literature for verification of data-aware processes. The former requires that quantification ranges over objects in the current active domain, while the latter additionally requires that objects assigned to variables persist across situations. Each of these two logics has a distinct corresponding notion of bisimulation. In spite of the differences we show that the two notions of bisimulation collapse for dynamic systems that are generic, which include all those systems specified through a situation calculus action theory. Then, by exploiting this result, we show that for bounded situation calculus action theories, mu-La and mu-Lp have exactly the same expressive power. Finally, we prove decidability of verification of mu-La properties over bounded action theories, using finite faithful abstractions. Differently from the mu-Lp case, these abstractions must depend on the number of quantified variables in the mu-La formula.

We will explore the use of disjunctive causal rules for representing indeterminate causation. We provide first a logical formalization of such rules in the form of a disjunctive inference relation, and describe its logical semantics. Then we consider a nonmonotonic semantics for such rules, described in (Turner 1999). It will be shown, however, that, under this semantics, disjunctive causal rules admit a stronger logic in which these rules are reducible to ordinary, singular causal rules. This semantics also tends to give an exclusive interpretation of disjunctive causal effects, and so excludes some reasonable models in particular cases. To overcome these shortcomings, we will introduce an alternative nonmonotonic semantics for disjunctive causal rules, called a covering semantics, that permits an inclusive interpretation of indeterminate causal information. Still, it will be shown that even in this case there exists a systematic procedure, that we will call a normalization, that allows us to capture precisely the covering semantics using only singular causal rules. This normalization procedure can be viewed as a kind of nonmonotonic completion, and it generalizes established ways of representing indeterminate effects in current theories of action.

Such a goal can represent either the behaviour model checking systems (e.g., MOCHA (Alur et al. 1998) of the computer system one wants to synthesize and Prism (Kwiatkowska, Norman, and Parker 2011)). Reactive (an automated design problem (Pnueli and Rosner 1989)) Modules supports succinct and high-level modelling or a particular system property which one wants to check of concurrent and multi-agent systems. In the games we (an automated verification problem (Clarke, Grumberg, and study, the preferences of system components are specified Peled 2000)). In this framework, it is assumed that the system by associating with each player in the game a temporal logic plays against an adversarial environment, that is, that (LTL) formula that the player desires to be satisfied. Reactive the goal of the environment is to prevent the system from Modules Games with perfect information (where each player achieving its goal. In game-theoretic terms, this means that can see the entire system state) have been extensively studied the problem is modelled as a zero-sum game, and hence that (Gutierrez, Harrenstein, and Wooldridge 2015a), but in its solution is given by the computation of a winning strategy this paper we focus on imperfect information cases. We study for either the system or the environment.

Generalized plans, such as plans with loops, are widely used in AI. Among other things, they are straightforward to execute, they allow action repetition, and they solve multiple problem instances. However, the correctness of such plans is non-trivial to define, making it difficult to provide a clear specification of what we should be looking for. Proposals in the literature, such as strong planning, are universally adopted by the community, but were initially formulated for finite state systems. There is yet to emerge a study on the sensitivity of such correctness notions to the structural assumptions of the underlying plan framework. In this paper, we are interested in the applicability and correctness of generalized plans in domains that are possibly unbounded, and/or stochastic, and/or continuous. To that end, we introduce a generic controller framework to capture different types of planning domains. Using this framework, we then study a number of termination and goal satisfaction criteria from first principles, relate them to existing proposals, and show plans that meet these criteria in the different types of domains.

Computing certain answers is the preferred way of answering queries in scenarios involving incomplete data. This, however, is computationally expensive, so practical systems use efficient techniques based on a particular three-valued logic, even though this often leads to incorrect results. Our goal is to provide a general many-valued framework for correctly approximating certain answers. We do so by defining the semantics of many-valued answers and queries, following the principle that additional knowledge about the input must translate into additional knowledge about the output. This framework lets us compare query outputs and evaluation procedures in terms of their informativeness. For each many-valued logic with a knowledge ordering on its truth values, one can build a syntactic evaluation procedure for all first-order queries, that correctly approximates certain answers; additional truth values are used to refine information about certain answers. For concrete examples, we show that a recently proposed approach fixing some of the inconsistencies of SQL query evaluation is an immediate consequence of our framework, and we further refine it by adding a fourth truth value. We show that no evaluation procedure based on Boolean logic delivers correctness guarantees. Finally, we study the relative power of evaluation procedures based on the informativeness of the answers they produce.

Bisimulation provides structural conditions to characterize indistinguishability between nodes on graph-like structures from an external observer. It is a fundamental notion used in many areas. However, many applications use graphs where nodes have data, and where observers can test for equality or inequality of data values (e.g., asking the attribute "name" of a node to be different from that of all its neighbors). The present work constitutes a first investigation of "data aware"' bisimulations on data graphs. We study the problem of computing such bisimulations, based on the observational indistinguishability for XPath — a language that extends modal logic with tests for data equality. We show that in general the problem is pspace-complete, but identify several restrictions that yield better complexity bounds (coNP, ptime) by controlling suitable parameters of the problem; namely, the amount of em non-locality allowed, and the class of models considered (graph, DAG, tree). In particular, this analysis yields a hierarchy of tractable fragments.

A principled way to study limited forms of reasoning for expressive knowledge bases is to specify the reasoning problem within a suitable logic of limited belief. Ideally such a logic comes equipped with a perspicuous semantics, which provides insights into the nature of the belief model and facilitates the study of the reasoning problem. While a number of such logics were proposed in the past, none of them is able to deal with function symbols except perhaps for the special case of logical constants. In this paper we propose a logic of limited belief with arbitrary function symbols. Among other things, we demonstrate that this form of limited belief has desirable properties such as eventual completeness for a large class of formulas and that it serves as a specification of a form of decidable reasoning for very expressive knowledge bases.

We study an epistemic logic where knowledge is built from what the agents observe (including higher-order visibility) and what the agents learn from public announcements. This fixes two main drawbacks of previous observability-based approaches where who sees what is common knowledge and where the epistemic operators distribute over disjunction. The latter forbids the modeling of most of the classical epistemic problems, starting with the muddy children puzzle. We integrate a dynamic dimension where both facts of the world and the agents’ observability can be modified by assignment programs. We establish that the model checking problem is PSPACE-complete.

In temporal logics, the operator F expresses that at some time in the future something happens, e.g., a request is eventually granted. Unfortunately, there is no bound on the time un- til the eventuality is satisfied which in many cases does not correspond to the intuitive meaning system designers have, namely, that F abstracts the idea that there is a bound on this time although its magnitude is not known. An elegant way to capture this meaning is through Prompt-LTL, which extends LTL with the operator F P ("prompt eventually"). We extend this work by studying alternating-time epistemic temporal logics extended with F P . We study the model-checking problem of the logic Prompt- KATL∗, which is ATL∗ extended with epistemic operators and prompt eventually. We also obtain results for the model-checking problem of some of its fragments. Namely, of Prompt-KATL (ATL with epistemic operators and prompt eventually), Prompt-KCTL∗ (CTL∗ with epistemic operators and prompt eventually), and finally the existential fragments of Prompt-KATL∗ and Prompt-KATL.