Publications
181 results found
, 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 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, 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: 48
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: 3
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
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
, 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
Lomuscio A, Nute D, 2005, Deontic Logic in Computer Science - Special Issue, Journal of Applied Logic, Vol: 3
Wozna B, Lomuscio A, Penczek W, 2005, Bounded model checking for knowledge and real time., Publisher: ACM, Pages: 165-172
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
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
, 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.
, 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.
, 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.
, 2004, Electronic Notes in Theoretical Computer Science: Preface, ISSN: 1571-0661
, 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 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
van der Hoek W, Lomuscio A, 2004, A logic for ignorance, DECLARATIVE AGENT LANGUAGES AND TECHNOLOGIES, Vol: 2990, Pages: 97-108, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 3
Raimondi F, Lomuscio A, 2004, Automatic verification of deontic interpreted systems by model checking via OBDD'S, 16th European Conference on Artificial Intelligence, Publisher: I O S PRESS, Pages: 53-57, ISSN: 0922-6389
, 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.
Lomuscio A, Sergot MJ, 2004, A formulation of violation, error recovery, and enforcement in the bit transmission problem, Journal of Applied Logic, Vol: 2
Kacprzak M, Lomuscio A, Lasica T, et al., 2004, Verifying Multi-agent Systems via Unbounded Model Checking., Publisher: Springer, Pages: 189-212
Lomuscio A, Sergot M, 2004, A formalisation of violation, error recovery, and enforcement in the bit transmission problem, Journal of Applied Logic, Vol: 2, Pages: 93-116, ISSN: 1570-8683
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.