References of "Penczek, Wojciech"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailStrategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them
Jamroga, Wojciech UL; Penczek, Wojciech; Sidoruk, Teofil

in Proceedings of KR 2021 (2021)

Detailed reference viewed: 29 (0 UL)
Full Text
Peer Reviewed
See detailMsATL: a Tool for SAT-Based ATL Satisfiability Checking
Niewiadomski, Artur; Kacprzak, Magdalena; Kurpiewski, Damian et al

in Proceedings of 19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020 (2020)

We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic ( ATL ) with imperfect informa- tion. MsATL combines SAT Modulo Monotonic Theories solvers with existing ... [more ▼]

We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic ( ATL ) with imperfect informa- tion. 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 imper- fect 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. [less ▲]

Detailed reference viewed: 40 (8 UL)
Full Text
Peer Reviewed
See detailMulti-valued Verification of Strategic Ability
Jamroga, Wojciech UL; Konikowska, Beata; Kurpiewski, Damian et al

in Fundamenta Informaticae (2020), 175(1-4), 207-251

Some multi-agent scenarios call for the possibility of evaluating specifications in aricher domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an ... [more ▼]

Some multi-agent scenarios call for the possibility of evaluating specifications in aricher domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic(mv-ATL∗→), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branching-time logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL∗→. We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL∗→. We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL∗→and motivate its use for model checking multi-agent systems. [less ▲]

Detailed reference viewed: 41 (0 UL)
Full Text
Peer Reviewed
See detailTowards Partial Order Reductions for Strategic Ability
Jamroga, Wojciech UL; Penczek, Wojciech; Sidoruk, Teofil et al

in Journal of Artificial Intelligence Research (2020), 68

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 27 (0 UL)
Full Text
Peer Reviewed
See detailTimed ATL: Forget Memory, Just Count
Knapik, Michal; André, Étienne; Petrucci, Laure et al

in Journal of Artificial Intelligence Research (2019), 66

Detailed reference viewed: 35 (0 UL)
Full Text
See detailSpecification and Verification of Multi-Agent Systems
Jamroga, Wojciech UL; Penczek, Wojciech

in Lectures on Logic and Computation (2012)

Detailed reference viewed: 110 (4 UL)