Publications
232 results found
Lomuscio A, Woźna B, 2007, A temporal epistemic logic with a reset operation, Pages: 574-581
We present an axiomatisation for an extension of a temporal epistemic logic with an epistemic "reset" operator defined on the intersection between epistemic and temporal relations. Additionally we show the logic has the finite model property, hence it is decidable. © 2007 IFAAMAS.
Belardinelli F, Lomuscio A, 2007, A quantified epistemic logic for reasoning about multi-agent systems, Pages: 601-603
We investigate quantified interpreted systems, a semantics for multiagent systems in which agents can reason about individuals, their properties, and the relationships among them. We analyse a first-order epistemic language interpreted on this semantics and show soundness and completeness of Q.S5n, an axiomatisation for these structures. © 2007 IFAAMAS.
Edelkamp S, Lomuscio A, 2007, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 4428 LNAI, ISSN: 0302-9743
Lomuscio A, Penczek W, 2007, Symbolic model checking for temporal-epistemic logics, Publisher: Association for Computing Machinery (ACM), Pages: 77-99, ISSN: 0163-5700
Lomuscio A, Qu H, Sergot M, et al., 2007, Verifying temporal and epistemic properties of web service compositions, 5th International Conference on Service-Oriented Computing (ICSOC 2007), Publisher: SPRINGER-VERLAG BERLIN, Pages: 456-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 6
Lomuscio A, Raimondi F, wozna B, 2007, Verification of the TESLA protocol in MCMAS-X, Workshop on the Concurrency Specification and Programming (CS&P), Publisher: IOS PRESS, Pages: 473-486, ISSN: 0169-2968
- Author Web Link
- Cite
- Citations: 2
Raimondi F, Lomuscio A, 2007, Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams, Journal of Applied Logic, Vol: 5, Pages: 235-251, ISSN: 1570-8683
Lomuscio A, Pecheur C, Raimondi F, 2007, Automatic Verification of Knowledge and Time with NuSMV, 20th International Joint Conference on Artificial Intelligence, Publisher: IJCAI-INT JOINT CONF ARTIF INTELL, Pages: 1384-1389
- Author Web Link
- Cite
- Citations: 29
Lomuscio A R, Penczek W, Wozna B, 2007, Bounded Model Checking for Knowledge and Real Time, roceedings of the 4th International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS'05), Publisher: Elsevier
Lomuscio A, Wozna B, Zbrzezny A, 2007, Bounded model checking real-time multi-agent systems with clock differences: theory and implementation, Mochart IV, Publisher: Springer
Lomuscio A, Penczek W, 2007, Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
, 2007, Model Checking and Artificial Intelligence, 4th Workshop, MoChArt IV, Riva del Garda, Italy, August 29, 2006, Revised Selected and Invited Papers, Publisher: Springer
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.
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: 17
van der Hoek W, Lomuscio A, de Vink E, et al., 2006, Preface, Pages: 1-2, ISSN: 1571-0661
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, Raimondi F, 2006, The complexity of model checking concurrent programs against CTLK specifications, Pages: 29-42, ISSN: 0302-9743
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.
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, 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: 77
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, 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, 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, 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, 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, Nute D, 2005, Editorial, Pages: 369-370, ISSN: 1570-8683
- Cite
- Citations: 3
Woźna B, Lomuscio A, Penczek W, 2005, Bounded model checking for knowledge and real time, AAMAS05: AAMAS '05 - Fourth International Joint Conference on Autonomous Agents and Multiagent Systems 2005, Publisher: ACM
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
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
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.