Author name cluster

Teofil Sidoruk

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

JAAMAS Journal 2026 Journal Article

Strategic (timed) computation tree logic

Jaime Arias
Wojciech Jamroga
Teofil Sidoruk

Abstract We define extensions of \(\textbf{CTL}\) and TCTL with strategic operators, called Strategic \(\textbf{CTL}\) ( SCTL ) and Strategic TCTL ( STCTL ), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i. e. STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTL \(_{{\textbf {ir}}}\) is of the same complexity as for ATL \(_{{\textbf {ir}}}\), the model checking problem for STCTL \(_{{\textbf {iR}}}\) is of the same complexity as for TCTL, while for STCTL \(_{{\textbf {iR}}}\) it is undecidable as for ATL \(_{{\textbf {iR}}}\). The above results suggest to use SCTL \(_{{\textbf {ir}}}\) and STCTL \(_{{\textbf {ir}}}\) in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTL \(_{{\textbf {ir}}}\).

Details DOI

AAMAS Conference 2026 Conference Paper

Towards Probabilistic Strategic Timed CTL

Wojciech Jamroga
Marta Kwiatkowska
Wojciech Penczek
Laure Petrucci
Teofil Sidoruk

We define PSTCTL, a probabilistic variant of Strategic Timed CTL (STCTL), interpreted over stochastic multi-agent systems with continuous time and asynchronous execution semantics. STCTL extends TCTL with strategic operators in the style of ATL. Moreover, we demonstrate the feasibility of verification with irP-strategies.

PDF

AAMAS Conference 2025 Conference Paper

Probabilistic Timed ATL

Wojciech Jamroga
Marta Kwiatkowska
Wojciech Penczek
Laure Petrucci
Teofil Sidoruk

We consider strategic reasoning for multi-agent systems modelled as networks of continuous-time probabilistic timed automata (TA) with asynchronous execution (PCAMAS) in the setting of imperfect information. We define PTATL, a probabilistic extension of the alternating-time timed temporal logic TATL, which is interpreted over PCAMAS. Focusing on memoryless strategies of agents with imperfect information, both probabilistic (irP) and deterministic (irp), we establish theoretical results regarding the computational complexity of model checking for the proposed logic: between PSPACE and EXPTIME for PTATLirp, and in 2EXPTIME for PTATLirP. We demonstrate the practical feasibility of verification for PTATLirp formulas through a novel proof-of-concept combination of state-of-the-art tools IMITATOR and PRISM on a scalable benchmark, with encouraging results.

PDF

AAMAS Conference 2023 Conference Paper

Strategic (Timed) Computation Tree Logic

Jaime Arias
Wojciech Jamroga
Wojciech Penczek
Laure Petrucci
Teofil Sidoruk

We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i. e. STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTLir is of the same complexity as for ATLir, the model checking problem for STCTLir is of the same complexity as for TCTL, while for STCTLiR it is undecidable as for ATLiR. The above results suggest to use SCTLir and STCTLir in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTLir.

PDF

AAMAS Conference 2021 Conference Paper

ADT2AMAS: Managing Agents in Attack-Defence Scenarios

Jaime Arias
Wojciech Penczek
Laure Petrucci
Teofil Sidoruk

Expressing attack-defence trees (ADTrees) in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance of attacking and defending strategies executed by agent coalitions. Our tool ADT2AMAS allows for transforming ADTrees into extended asynchronous multi-agent systems and computing an optimal schedule with the minimal number of agents. ADT2AMAS is integrated within the graphical verification platform CosyVerif, but can also be run standalone.

PDF

AAMAS Conference 2021 Conference Paper

Strategic Abilities of Asynchronous Agents: Semantic Side Effects

Wojciech Jamroga
Wojciech Penczek
Teofil Sidoruk

Recently, we have proposed a framework for verification of agents’ abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models [14, 16]. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies.

PDF

KR Conference 2021 Conference Paper

Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them

Wojciech Jamroga
Wojciech Penczek
Teofil Sidoruk

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems (MAS), together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

PDF Details DOI

JAIR Journal 2020 Journal Article

Towards Partial Order Reductions for Strategic Ability

Wojciech Jamroga
Wojciech Penczek
Teofil Sidoruk
Piotr Dembiński
Antoni Mazurkiewicz

We propose a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information. Based on the semantics, we show some general complexity results for verification of strategic abilities in asynchronous interaction. More importantly, we develop a methodology for partial order reduction in verification of agents with imperfect information. We show that the reduction preserves an important subset of strategic properties, with as well as without the fairness assumption. We also demonstrate the effectiveness of the reduction on a number of benchmarks. Interestingly, the reduction does not work for strategic abilities under perfect information.

PDF Details DOI