arXiv subjects

Michał Knapik

Publications and source records attributed to Michał Knapik.

5 recordsLinked to original sources

arXiv2023

MsATL: a Tool for SAT-Based ATL Satisfiability Checking

We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic (ATL) with imperfect information. MsATL combines SAT Modulo Monotonic Theories solvers with existing ATL model checkers: MCMAS and STV. The tool can deal with various semantics of ATL, including perfect and imperfect information, and can handle additional practical requirements. MsATL can be applied for synthesis of games that conform to a given specification, with the synthesised game often being minimal.

cs.LO↗

arXiv2020

Modular Analysis of Tree-Topology Models

We investigate networks of automata that synchronise over common action labels. A graph synchronisation topology between the automata is defined in such a way that two automata are connected iff they can synchronise over an action. We show a very effective reduction of networks of automata with tree-like synchronisation topologies. The reduction preserves a certain form of reachability, but not safety. The procedure is implemented in an open-source tool.

cs.LO↗

arXiv2019

Parametric Verification: An Introduction

This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toruń (2016) and Zaragoza (2017). The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area. We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.

cs.LO↗

arXiv2017

Fixpoint Approximation of Strategic Abilities under Imperfect Information

Model checking of strategic ability under imperfect information is known to be hard. The complexity results range from NP-completeness to undecidability, depending on the precise setup of the problem. No less importantly, fixpoint equivalences do not generally hold for imperfect information strategies, which seriously hampers incremental synthesis of winning strategies. In this paper, we propose translations of ATLir formulae that provide lower and upper bounds for their truth values, and are cheaper to verify than the original specifications. That is, if the expression is verified as true then the corresponding formula of ATLir should also hold in the given model. We begin by showing where the straightforward approach does not work. Then, we propose how it can be modified to obtain guaranteed lower bounds. To this end, we alter the next-step operator in such a way that traversing one's indistinguishability relation is seen as atomic activity. Most interestingly, the lower approximation is provided by a fixpoint expression that uses a nonstandard variant of the next-step ability operator. We show the correctness of the translations, establish their computational complexity, and validate the approach by experiments with a scalable scenario of Bridge play.

cs.MA↗

arXiv2016

Approximating Strategic Abilities under Imperfect Information: a Naive Approach

Alternating-time temporal logic (ATL) allows to specify requirements on abilities that different agents should (or should not) possess in a multi-agent system. However, model checking ATL specifications in realistic systems is computationally hard. In particular, if the agents have imperfect information about the global state of the system, the complexity ranges from Delta2P to undecidable, depending on the syntactic and semantic details. The problem is also hard in practice, as evidenced by several recent attempts to tackle it. On the other hand, model checking of alternating epistemic mu-calculus can have a distinctly lower computational complexity. In this work, we look at the idea of approximating the former problem by the verification of its "naive" translations to the latter. In other words, we look at what happens when one uses the (incorrect) fixpoint algorithm to verify formulae of ATL with imperfect information.

cs.MA↗