Browse ORBilu by Open Access
- What it is and what it isn't
- Green Road / Gold Road?
- Ready to Publish. Now What?
- How can I support the OA movement?
- Where can I learn more?
ORBilu is a project developed by
   Strategic Abilities of Asynchronous Agents: Semantic Side EffectsJamroga, Wojciech  ; ; in Proceedings of AAMAS 2021 (2021) Detailed reference viewed: 45 (5 UL)Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame ThemJamroga, Wojciech ; ; in Proceedings of KR 2021 (2021) Detailed reference viewed: 59 (6 UL)Towards Partial Order Reductions for Strategic AbilityJamroga, Wojciech ; ; et alin 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: 44 (0 UL) Multi-valued Verification of Strategic AbilityJamroga, Wojciech ; ; et alin 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: 54 (0 UL)MsATL: a Tool for SAT-Based ATL Satisfiability Checking; ; 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: 50 (8 UL)Timed ATL: Forget Memory, Just Count; ; et al in Journal of Artificial Intelligence Research (2019), 66 Detailed reference viewed: 48 (0 UL)Specification and Verification of Multi-Agent SystemsJamroga, Wojciech ; in Lectures on Logic and Computation (2012) Detailed reference viewed: 121 (4 UL) |
||
