Browsing ORBilu

MyORBi^lu

Browse ORBi^lu by

Open Access

ORBi^lu

The ORBi^lu Project

ISSN: 2354-5011

ORBi^lu is a project developed by


	References of "Jamroga, Wojciech 50035886" in Showing results 1 to 20 of 59 1 2 3 Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them Jamroga, Wojciech ; Penczek, Wojciech; Sidoruk, Teofil in Proceedings of KR 2021 (2021) Detailed reference viewed: 69 (6 UL) STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions Kurpiewski, Damian; Pazderski, Witold; Jamroga, Wojciech et al in Proceedings of AAMAS (2021) Detailed reference viewed: 41 (3 UL) A Survey of Requirements for COVID-19 Mitigation Strategies Jamroga, Wojciech ; Mestel, David ; Roenne, Peter et al in Bulletin of The Polish Academy of Sciences: Technical Science (2021), 69(4), 137724 Detailed reference viewed: 83 (4 UL) Bisimulations 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: 75 (13 UL) A Declaration of Software Independence Jamroga, Wojciech ; Ryan, Peter Y A ; Schneider, Steve et al in Protocols, Strands, and Logic - Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday (2021) Detailed reference viewed: 87 (4 UL) Strategic Abilities of Asynchronous Agents: Semantic Side Effects Jamroga, Wojciech ; Penczek, Wojciech; Sidoruk, Teofil in Proceedings of AAMAS 2021 (2021) Detailed reference viewed: 50 (5 UL) A Survey of Requirements for COVID-19 Mitigation Strategies. Part II: Elicitation of Requirements Jamroga, Wojciech 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: 77 (13 UL) Towards Partial Order Reductions for Strategic Ability Jamroga, Wojciech ; 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: 55 (0 UL) Multi-valued Verification of Strategic Ability Jamroga, Wojciech ; 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: 65 (0 UL) MsATL: 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: 59 (8 UL) A Survey of Requirements for COVID-19 Mitigation Strategies. Part I: Newspaper Clips Jamroga, Wojciech ; Mestel, David ; Roenne, Peter et al E-print/Working paper (2020) Detailed reference viewed: 122 (6 UL) Towards Model Checking of Voting Protocols in Uppaal Jamroga, Wojciech ; Kim, Yan ; 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: 135 (10 UL) Natural Strategic Abilities in Voting Protocols Jamroga, Wojciech ; 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: 55 (2 UL) Reasoning about Strategic Abilities: Agents with Truly Perfect Recall Bulling, Nils; Jamroga, Wojciech ; Popovici, Matei in ACM Transactions on Computational Logic (2019), 20(2), 101--1046 Detailed reference viewed: 32 (0 UL) Risk-Limiting Tallies Jamroga, Wojciech ; Roenne, Peter ; Ryan, Peter et al in Electronic Voting: Proceedings of E-Vote-ID (2019) Detailed reference viewed: 81 (5 UL) Natural Strategic Ability Jamroga, Wojciech ; Malvone, Vadim; Murano, Aniello in Artificial Intelligence and Law (2019), 277 Detailed reference viewed: 65 (2 UL) On Domination and Control in Strategic Ability (Extended Abstract) Kurpiewski, Damian; Knapik, Michal; Jamroga, Wojciech in Proceedings of the 31st Benelux Conference on Artificial Intelligence (BNAIC) (2019) Detailed reference viewed: 31 (0 UL) Approximate Verification of Strategic Abilities under Imperfect Information Jamroga, Wojciech ; Knapik, Micha L; Kurpiewski, Damian et al in Artificial Intelligence and Law (2019), 277 Detailed reference viewed: 76 (2 UL) Strategic 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: 46 (0 UL) STV: Model Checking for Strategies under Imperfect Information Kurpiewski, Damian; Jamroga, Wojciech ; Knapik, Micha L in Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019 (2019) Detailed reference viewed: 44 (1 UL) 1 2 3

Creative Commons Licence

University of Luxembourg Library | Feedback | Legal notices