Publications
187 results found
Lomuscio A, Woźna B, 2006, A complete and decidable security-specialised logic and its application to the TESLA protocol, Pages: 145-152
We examine a logic to reason about security protocols by means of temporal and epistemic concepts. We report results on completeness and decidability of the formalism as well as its expressiveness. As a case study we apply the formalism in the analysis of TESLA, a secure stream multi-cast protocol. Copyright 2006 ACM.
Lomuscio A, Raimondi F, 2006, Model checking knowledge, strategies, and games in multi-agent systems, Pages: 161-168
We present an OBDD-based methodology for verifying time, knowledge, and strategies in multi-agent systems specified by the formalism of interpreted systems. To this end, we investigate the interpretation of ATL and epistemic formulae in various classes of interpreted systems, we present model checking algorithms and their implementation, and report experimental results. Copyright 2006 ACM.
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
Lomuscio A, Raimondi F, 2006, MCMAS: A Model Checker for Multi-agent Systems
- Cite
- Citations: 81
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, 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, 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, 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: 50
Lomuscio A, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Conference on Precision Electromagnetic Measurements (CPEM 06), Publisher: SPRINGER-VERLAG BERLIN, Pages: 29-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 4
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
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
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, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications., Publisher: ACM, Pages: 548-550
Lomuscio A, Nute D, 2005, Editorial, Pages: 369-370, ISSN: 1570-8683
- Cite
- Citations: 2
Woźna B, Lomuscio A, Penczek W, 2005, Bounded model checking for deontic interpreted systems, Electronic Notes in Theoretical Computer Science, Vol: 126, Pages: 93-114, ISSN: 1571-0661
We propose a framework for the verification of multi-agent systems' specification by symbolic model checking. The language CTLKD (an extension of CTL) allows for the representation of the temporal evolution of epistemic states of the agents, as well as their correct and incorrect functioning behaviour. We ground our analysis on the semantics of deontic interpreted systems. The verification approach is based on an adaption of the technique of bounded model checking, a mainstream approach in verification of reactive systems. We test our results on a typical communication scenario: the bit transmission problem with faults.
Kacprzak M, Lomuscio A, Lasica T, et al., 2005, Verifying multi-agent systems via unbounded model checking, 3rd International Workshop on Formal Approaches to Agent-Based Systems (FAABS 2004), Publisher: SPRINGER-VERLAG BERLIN, Pages: 189-212, ISSN: 0302-9743
- Author Web Link
- 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, 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.
Van Der Hoek W, Lomuscio A, De Vink E, et al., 2004, Electronic Notes in Theoretical Computer Science: Preface, ISSN: 1571-0661
Raimondi F, Lomuscio A, 2004, A tool for specification and verification of epistemic properties in interpreted systems, Electronic Notes in Theoretical Computer Science, Vol: 85, Pages: 176-191, ISSN: 1571-0661
We present a compiler that translates a multi-agent systems specification given in the formalism of Interpreted Systems into an SMV program. We show how an SMV model checker can be coupled with a Kripke model editor (Akka) to allow for the mechanical verification of epistemic properties of multi-agent systems. We apply this methodology to the verification of a communication protocol - the dining cryptographers. © 2004 Published by Elsevier Science B.V.
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
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.
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.