Publications
187 results found
Lomuscio A, Penczek W, 2007, Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
Van Der Hoek W, Lomuscio A, Wooldridge M, 2006, On the complexity of practical ATL model checking, Pages: 201-208
We investigate the computational complexity of reasoning about multi-agent systems using the cooperation logic ATL of Alur, Henzinger, and Kupferman. It is known that satisfiability checking is EXPTIME-complete for "full" ATL, and PSPACE-complete (in the general case) for the fragment of ATL corresponding to Pauly's Coalition Logic. In contrast, the model checking problems for ATL and Coalition Logic can both be solved in time polynomial in the size of the formula and the size of model against which the formula is to be checked. However, these latter results assume an extensive representation of models, in which all states of a model are explicitly enumerated. Such representations are not feasible in practice. In this paper we investigate the complexity of the ATL and Coalition Logic model checking problems for a more "reasonable" model representation known as SRML ("Simple Reactive Modules Language"), a simplified version of the actual model representation languages used for model checkers such as SMV and MOCHA. While it is unsurprising that, when measured against such representations, the model checking problems for ATL and Coalition Logic have a higher complexity than when measured against explicit state representations, we show that in fact the ATL and Coalition Logic model checking problems for SRML models have the same complexity as the corresponding satisfiability problems. That is, model checking ATL formulae against SRML models is EXPTIME-complete, and model checking Coalition Logic formulae against SRML models is PSPACE-complete. We conclude by investigating some technical issues around these results, and discussing their implications. Copyright 2006 ACM.
Lomuscio AR, Pecheur C, Raimondi F, 2006, Verification of knowledge and time with NuSMV., Twentieth International Conference on Artificial Intelligence
Kacprzak M, Lomuscio A, Niewiadomski A, et al., 2006, Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol, Meeting on Concurrency Specification and Programming, Publisher: IOS PRESS, Pages: 215-234, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 13
van der Hoek W, Lomuscio A, de Vink E, et al., 2006, Preface, Pages: 1-2, ISSN: 1571-0661
Lomuscio A, Wozna B, 2006, A complete and decidable axiomatisation for deontic interpreted systems, 8th International Workshop on Deontic Logic in Computer Science (DEON 2006), Publisher: SPRINGER-VERLAG BERLIN, Pages: 238-254, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 4
Lomuscio A, Raimondi F, 2006, Model checking knowledge, strategies, and games in multi-agent systems, Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM
Lomuscio A, Wozna B, 2006, A combination of explicit and deductive knowledge with branching time: Completeness and decidability results, 3rd International Workshop on Declarative Agent Languages and Technologies, Publisher: SPRINGER-VERLAG BERLIN, Pages: 188-204, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 1
Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Pages: 29-42, ISSN: 0302-9743
© Springer-Verlag Berlin Heidelberg 2006. This paper presents complexity results for model checking formulae of CTLK (a logic to reason about time and knowledge in multi-agent systems) in concurrent programs. We apply these results to evaluate the complexity of verifying programs of two model checkers for multi-agent systems: MCMAS and Verics.
Lomuscio A, Raimondi F, 2006, MCMAS: A model checker for multi-agent systems, 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 450-454, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 54
van der Hoek W, Lomuscio A, Wooldridge M, 2006, On the complexity of practical ATL model checking knowledge, strategies, and games in multi-agent systems, Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM
Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Proceedings of 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM
Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications., Publisher: ACM, Pages: 548-550
van der Hoek W, Lomuscio A, de Vink E, et al., 2006, Proceedings of LCMAS05 - Special issue, Electronic Notes of Theoretical Computer Science, Vol: 126
Lomuscio A, Wozna B, 2006, A complete and decidable security-specialised logic and its application to the TESLA protocol, Proceedings of 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS06), Publisher: ACM
Lomuscio A, Nute D, 2005, Editorial, Pages: 369-370, ISSN: 1570-8683
- Cite
- Citations: 2
Raimondi F, Lomuscio A, 2005, Towards symbolic model checking for multi-agent systems via OBDD's, 3rd International Workshop on Formal Approaches to Agent-Based Systems (FAABS 2004), Publisher: SPRINGER-VERLAG BERLIN, Pages: 213-221, ISSN: 0302-9743
van der Hoek W, Lomuscio A, de Vink E, et al., 2005, Proceedings of LCMAS04 - Special Issue, Electronic Notes of Theoretical Computer Science, Vol: 126
Wozna B, Lomuscio A, Penczek W, 2005, Bounded model checking for knowledge and real time., Publisher: ACM, Pages: 165-172
Lomuscio A, Nute D, 2005, Deontic Logic in Computer Science - Special Issue, Journal of Applied Logic, Vol: 3
Kacprzak M, Lomuscio A, Penczek W, 2004, From bounded to unbounded model checking for temporal epistemic logic, FUNDAMENTA INFORMATICAE, Vol: 63, Pages: 221-240, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 8
Kacprzak M, Lomuscio A, Penczek W, 2004, Verification of multiagent systems via unbounded model checking, Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2004, Vol: 2, Pages: 638-645
We present an approach to the problem of verification of epistemic properties of multi-agent systems by means of symbolic model checking. In particular, it is shown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we base our discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show how it can be applied to the well-known train, gate and controller problem.
Raimondi F, Lomuscio A, 2004, Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation, Pages: 630-637
We investigate the problem of the verification of epistemic properties of multiagent systems via model checking. Specifically, we extend and adapt methods based on ordered binary decision diagrams, a mainstream verification technique in reactive systems. We provide an algorithm, and present a software package that implements it. We discuss the software and benchmark it by means of a standard example in the literature, the dining cryptographers.
Van Der Hoek W, Lomuscio A, De Vink E, et al., 2004, Electronic Notes in Theoretical Computer Science: Preface, ISSN: 1571-0661
Van Der Hoek W, Lomuscio A, 2004, A logic for ignorance, Pages: 117-133, ISSN: 1571-0661
We introduce and motivate a non-standard multi-modal logic to represent and reason about ignorance in Multi-Agent Systems. We argue that in Multi-agent systems being able to reason about what agents ignore is just as important as being able to reason about what agents know. We show a sound and complete axiomatisation for the logic. We investigate its applicability by restating the feasibility condition for the FIPA communication primitive of inform. © 2004 Published by Elsevier Science B.V.
Raimondi F, Lomuscio A, 2004, Automatic verification of deontic interpreted systems by model checking via OBDD's, Pages: 48-52, ISSN: 0922-6389
We present an algorithm for the verification of multiagent systems specified by means of a modal logic that includes a temporal, an epistemic, and a deontic operator. Verification is performed by model checking on OBDD's. We present an implementation of the algorithm and report on experimental results for the bit transmission problem with faults.
Raimondi F, Lomuscio A, 2004, Automatic verification of deontic properties of multi-agent systems, 7th International Workshop on Deontic Logic in Computer Science, Publisher: SPRINGER-VERLAG BERLIN, Pages: 228-242, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 1
Wozna B, Lomuscio A, 2004, A logic for knowledge, correctness, and real time, 5th International Workshop on Computational Logic in Multi-Agent Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 1-15, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 4
van der Hoek W, Lomuscio A, 2004, A Logic for Ignorance, Electronic Notes of Theoretical Computer Science, Vol: 85
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.