References of "Jamroga, Wojciech 50035886"
     in
Bookmark and Share    
See detailA Survey of Requirements for COVID-19 Mitigation Strategies. Part II: Elicitation of Requirements
Jamroga, Wojciech UL

E-print/Working paper (2021)

The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies, based on social, political, and technological instruments ... [more ▼]

The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies, based on social, political, and technological instruments. We postulate that multi-agent systems can provide a common platform to study (and balance) their essential properties. We also show how to obtain a comprehensive list of the properties by ``distilling'' them from media snippets. Finally, we present a preliminary take on their formal specification, using ideas from multi-agent logics. [less ▲]

Detailed reference viewed: 54 (4 UL)
Full Text
Peer Reviewed
See detailBisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting Protocol
Belardinelli, Francesco; Condurache, Rodica; Dima, Catalin et al

in Information and Computation (2021), 276

We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL$^*$ for both the {\em objective} and {\em subjective ... [more ▼]

We propose a notion of alternating bisimulation for strategic abilities under imperfect information. The bisimulation preserves formulas of ATL$^*$ for both the {\em objective} and {\em subjective} variants of the state-based semantics with imperfect information, which are commonly used in the modeling and verification of multi-agent systems. Furthermore, we apply the theoretical result to the verification of coercion-resistance in the ThreeBallot voting system, a voting protocol that does not use cryptography. In particular, we show that natural simplifications of an initial model of the protocol are in fact bisimulations of the original model, and therefore satisfy the same ATL$^*$ properties, including coercion-resistance. These simplifications allow the model-checking tool MCMAS to terminate on models with a larger number of voters and candidates, compared with the initial model. [less ▲]

Detailed reference viewed: 35 (2 UL)
Full Text
Peer Reviewed
See detailTowards Model Checking of Voting Protocols in Uppaal
Jamroga, Wojciech UL; Kim, Yan UL; Kurpiewski, Damian et al

in Proceedings of the Fifth International Joint Conference on Electronic Voting E-VOTE-ID 2020 (2020)

The design and implementation of a trustworthy e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting ... [more ▼]

The design and implementation of a trustworthy e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting system works, and what requirements on the system are relevant. In this paper, we propose that the state-of-art model checker Uppaal provides a good environment for modelling and preliminary verification of voting protocols. To illustrate this, we demonstrate how to model a version of Pret-a-Voter in Uppaal, together with some natural extensions. We also show how to verify a variant of receipt-freeness, despite the severe limitations of the property specification language in the model checker. The aim of this work is to open a new path, rather then deliver the ultimate outcome of formal analysis. A comprehensive model of Pret-a-Voter, more accurate specification of requirements, and exhaustive verification are planned for the future. [less ▲]

Detailed reference viewed: 61 (1 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: 38 (6 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 detailNatural Strategic Abilities in Voting Protocols
Jamroga, Wojciech UL; Kurpiewski, Damian; Malvone, Vadim

in Proceedings of the 10th International Workshop on Socio-Technical Aspects in Security STAST 2020 (2020)

Security properties are often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the property at hand. In real life, this ... [more ▼]

Security properties are often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the property at hand. In real life, this cannot be taken for granted. In particular, security mechanisms that are difficult and costly to use are often ignored by the users, and do not really defend the system against possible attacks.Here, we propose a graded notion of security based on the complexity of the user’s strategic behavior. More precisely, we suggest that the level to which a security property φ is satisfied can be defined in terms of (a)the complexity of the strategy that the voter needs to execute to make φ true, and (b) the resources that the user must employ on the way. The simpler and cheaper to obtain φ, the higher the degree of security. We demonstrate how the idea works in a case study based on an electronicv oting scenario. To this end, we model the vVote implementation of thePrˆet `a Voter voting protocol for coercion-resistant and voter-verifiable elections. Then, we identify “natural” strategies for the voter to obtain receipt-freeness, and measure the voter’s effort that they require. We also look at how hard it is for the coercer to compromise the election through a randomization attack. [less ▲]

Detailed reference viewed: 33 (2 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
Peer Reviewed
See detailOn Domination and Control in Strategic Ability (Extended Abstract)
Kurpiewski, Damian; Knapik, Michal; Jamroga, Wojciech UL

in Proceedings of the 31st Benelux Conference on Artificial Intelligence (BNAIC) (2019)

Detailed reference viewed: 14 (0 UL)
Full Text
Peer Reviewed
See detailSome Things are Easier for the Dumb and the Bright Ones (Beware the Average!)
Jamroga, Wojciech UL; Knapik, Michal

in Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence IJCAI (2019)

Detailed reference viewed: 37 (0 UL)
Full Text
Peer Reviewed
See detailNatural Strategic Ability
Jamroga, Wojciech UL; Malvone, Vadim; Murano, Aniello

in Artificial Intelligence and Law (2019), 277

Detailed reference viewed: 39 (2 UL)
Full Text
Peer Reviewed
See detailSTV: Model Checking for Strategies under Imperfect Information
Kurpiewski, Damian; Jamroga, Wojciech UL; Knapik, Micha L

in Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019 (2019)

Detailed reference viewed: 21 (0 UL)
Full Text
Peer Reviewed
See detailRisk-Limiting Tallies
Jamroga, Wojciech UL; Roenne, Peter UL; Ryan, Peter UL et al

in Electronic Voting: Proceedings of E-Vote-ID (2019)

Detailed reference viewed: 35 (5 UL)
Full Text
Peer Reviewed
See detailStrategic Responsibility Under Imperfect Information
Yazdanpanah, Vahid; Dastani, Mehdi; Alechina, Natasha et al

in Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019 (2019)

Detailed reference viewed: 26 (0 UL)
Full Text
Peer Reviewed
See detailApproximate Verification of Strategic Abilities under Imperfect Information
Jamroga, Wojciech UL; Knapik, Micha L; Kurpiewski, Damian et al

in Artificial Intelligence and Law (2019), 277

Detailed reference viewed: 46 (2 UL)
Full Text
Peer Reviewed
See detailOn Domination and Control in Strategic Ability
Kurpiewski, Damian; Knapik, Micha L; Jamroga, Wojciech UL

in Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019 (2019)

Detailed reference viewed: 17 (0 UL)
Full Text
Peer Reviewed
See detailReasoning about Strategic Abilities: Agents with Truly Perfect Recall
Bulling, Nils; Jamroga, Wojciech UL; Popovici, Matei

in ACM Transactions on Computational Logic (2019), 20(2), 101--1046

Detailed reference viewed: 18 (0 UL)
Full Text
Peer Reviewed
See detailNatural Strategic Ability under Imperfect Information
Jamroga, Wojciech UL; Malvone, Vadim; Murano, Aniello

in Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019 (2019)

Detailed reference viewed: 17 (0 UL)
Full Text
Peer Reviewed
See detailStrategy Logic with Simple Goals: Tractable Reasoning about Strategies
Belardinelli, Francesco; Jamroga, Wojciech UL; Kurpiewski, Damian et al

in Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence IJCAI (2019)

Detailed reference viewed: 37 (1 UL)