Conformance checking is a process mining task where observed process executions are compared with the conduct prescribed by a process model. Even in the case where multiple parties interact in the process, it is typically assumed that the process itself provides a monolithic, global description of the overall, expected behaviour. However, it may very well be the case that such a global process is not explicitly available, and that each agent comes with its own local view of the process, while the overall behaviour is only be implicitly obtained by composing such local views. In this paper, we provide for the first time a formal framework for glocal conformance checking, where a global observed trace of a multi-party process is related to local Data Petri nets, each representing the subjective view of each participating agent. We formulate conformance checking in this multi-agent setting as an alignment problem, and show how it can be tackled by “acting locally, and thinking globally”, that is, pairing local alignments with a suitable global compatibility condition. We then observe that in this setting, cost functions must take the context of activities in the global trace into account, which is realised through a new schema of regular expression-based cost functions. We pair the foundational investigation of the problem with a proof-of-concept SMT-based implementation.

Bisimulations are standard in modal logic and, more generally, in the theory of state-transition systems. The quotient structure of a Kripke model with respect to the bisimulation relation is called a bisimulation contraction. The bisimulation contraction is a minimal model bisimilar to the original model, and hence, for (image-)finite models, a minimal model modally equivalent to the original. Similar definitions exist for bounded bisimulations ($k$-bisimulations) and bounded bisimulation contractions. Two finite models are $k$-bisimilar if and only if they are modally equivalent up to modal depth $k$. However, the quotient structure with respect to the $k$-bisimulation relation does not guarantee a minimal model preserving modal equivalence to depth $k$. In this paper, we remedy this asymmetry to standard bisimulations and provide a novel definition of bounded contractions called rooted $k$-contractions. We prove that rooted $k$-contractions preserve $k$-bisimilarity and are minimal with this property. Finally, we show that rooted $k$-contractions can be exponentially more succinct than standard $k$-contractions.

The use of Dynamic Epistemic Logic (DEL) in multi-agent planning has led to a widely adopted action formalism that can handle nondeterminism, partial observability and arbitrary knowledge nesting. As such expressive power comes at the cost of undecidability, several decidable fragments have been isolated, mainly based on syntactic restrictions of the action formalism. In this paper, we pursue a novel semantic approach to achieve decidability. Namely, rather than imposing syntactical constraints, the semantic approach focuses on the axioms of the logic for epistemic planning. Specifically, we augment the logic of knowledge S5$_n$ and with an interaction axiom called (knowledge) commutativity, which controls the ability of agents to unboundedly reason on the knowledge of other agents. We then provide a threefold contribution. First, we show that the resulting epistemic planning problem is decidable. In doing so, we prove that our framework admits a finitary non-fixpoint characterization of common knowledge, which is of independent interest. Second, we study different generalizations of the commutativity axiom, with the goal of obtaining decidability for more expressive fragments of DEL. Finally, we show that two well-known epistemic planning systems based on action templates, when interpreted under the setting of knowledge, conform to the commutativity axiom, hence proving their decidability.

Dynamic Epistemic Logic (DEL) provides a framework for epistemic planning that is capable of representing non-deterministic actions, partial observability, higher-order knowledge and both factual and epistemic change. The high expressivity of DEL challenges existing epistemic planners, which typically can handle only restricted fragments of the whole framework. The goal of this work is to push the envelop of practical DEL planning, ultimately aiming for epistemic planners to be able to deal with the full range of features offered by DEL. Towards this goal, we question the traditional semantics of DEL, defined in terms on Kripke models. In particular, we propose an equivalent semantics defined using, as main building block, so-called possibilities: non well-founded objects representing both factual properties of the world, and what agents consider to be possible. We call the resulting framework DELPHIC. We argue that DELPHIC indeed provides a more compact representation of epistemic states. To substantiate this claim, we implement both approaches in ASP and we set up an experimental evaluation to compare DELPHIC with the traditional, Kripke-based approach. The evaluation confirms that DELPHIC outperforms the traditional approach in space and time.

Epistemic planning is a branch of Artificial Intelligence that stems from the combination of automated planning and Dynamic Epistemic Logic (DEL). While DEL provides a very expressive framework—which comes at the cost of undecidability—to guarantee the feasibility of the planning process, various fragments have been studied in the literature, that rely on very specific syntax for representing domains. As a result, a comprehensive language that is able to capture the general DEL framework is currently not present in the literature. In this paper, we propose a new language called EPDDL (Epistemic Planning Domain Definition Language), through which we can capture the full DEL semantics, thus allowing for a general and unified syntax for representing epistemic planning domains.

Dynamic Epistemic Logic (DEL) provides a very expressive framework for planning, called epistemic planning. In this paper, we discuss the shortcomings of the traditional DEL semantics, based on Kripke models, and we propose a formulation of epistemic planning based on a different kind of object, called possibility. We argue that the resulting framework, named DELPHIC, constitutes a valid alternative, since it provides a more compact representation of epistemic information and a lighter update mechanism. We conclude by discussing the advantages of DELPHIC, both theoretically and in terms of implementation.

Developing autonomous agents that can reason about the perspective of their (human or artificial) peers is paramount to realistically model a variety of real-world domains. Being aware of the state of mind of others is a key aspect in different fields—e.g., legal reasoning, business negotiations, ethical AI and explainable AI. In particular, in the area of Multi-Agent Epistemic Planning (MEP), agents must reach their goals by taking into account the knowledge and beliefs of other agents. Although the literature offers an ample spectrum of approaches for planning in this scenario, they often come with limitations. This paper expands previous formalization of MEP to enable representing and reasoning in presence of inconsistent beliefs of agents, trust relations and lies. The paper explores the syntax and semantics of the extended MEP framework, along with an implementation of the framework in the solver Epistemic Forward Planner (EFP). The paper reports formal properties about the newly introduced epistemic states update that have been also empirically tested via an actual implementation of the solver.

Designing agents that reason and act upon the world has always been one of the main objectives of the Artificial Intelligence community. While for planning in “simple” domains the agents can solely rely on facts about the world, in several contexts, e.g., economy, security, justice and politics, the mere knowledge of the world could be insufficient to reach a desired goal. In these scenarios, epistemic reasoning, i.e., reasoning about agents’ beliefs about themselves and about other agents’ beliefs, is essential to design winning strategies. This paper addresses the problem of reasoning in multi-agent epistemic settings exploiting declarative programming techniques. In particular, the paper presents an actual implementation of a multi-shot Answer Set Programming-based planner that can reason in multi-agent epistemic settings, called PLATO (ePistemic muLti-agent Answer seT programming sOlver). The ASP paradigm enables a concise and elegant design of the planner, w.r.t. other imperative implementations, facilitating the development of formal verification of correctness. The paper shows how the planner, exploiting an ad-hoc epistemic state representation and the efficiency of ASP solvers, has competitive performance results on benchmarks collected from the literature.

Multi-agent systems have been employed to model, simulate and explore a variety of real-world scenarios. It is becoming more and more important to investigate formalisms and tools that would allow us to exploit automated reasoning in these domains. An area that has received increasing attention is the use of multi-agent systems which allow an agent to reason about the knowledge and beliefs of other agents. This type of reasoning, i.e., about agents’ perception of the world and also about agents’ knowledge of her and others’ knowledge, is referred to as epistemic reasoning. This paper presents an updated formalization and implementation of a multi-agent epistemic planner, called EFP. In particular, the paper explores the advantages of using alternative state representations that deviate from the commonly used Kripke structures. The paper explores such alternatives in the context of an action language for multi-agent epistemic planning. The paper presents also an actual implementation of a planner that uses the novel ideas, demonstrating concrete performance improvements on benchmarks collected from the literature.