Article

Abstractions of Multi-agent Systems

Authors:

CEEMAS '07: Proceedings of the 5th international Central and Eastern European conference on Multi-Agent Systems and Applications V

Pages 11 - 21

https://doi.org/10.1007/978-3-540-75254-7_2

Published: 25 September 2007 Publication History

Abstract

With the recent development of many model-checkers for the temporal logic of knowledge, abstraction techniques are necessary to increase the size of the systems that can be verified. In this paper, we introduce several abstraction techniques for interpreted systems and we prove several preservation results. These results consider the temporal logic of knowledge under Kleene's 3-valued interpretation along infinite and maximal finite paths.

References

[1]

Chechik, M., Easterbrook, S.M., Petrovykh, V.: Model-checking over multivalued logics. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 72-98. Springer, Heidelberg (2001).

Crossref

Google Scholar

[2]

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238-252 (1977).

Crossref

Google Scholar

[3]

Dams, D.: Abstract Interpretation and Partial Refinement for Model Checking. PhD thesis, Technische Universität Eindhoven (1996).

Google Scholar

[4]

Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995).

Crossref

Google Scholar

[5]

Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479-483. Springer, Heidelberg (2004).

Google Scholar

[6]

Ginsberg, M.: Multivalued logics. A uniform approach to inference in artificial intelligence. Computational Intelligence 4, 265-316 (1988).

Google Scholar

[7]

Konikowska, B., Penczek, W.: Model checking for multivalued logic of knowledge and time. In: Proceedings of AAMAS, pp. 169-176 (2006).

Crossref

Google Scholar

[8]

Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 450-454. Springer, Heidelberg (2006).

Crossref

Google Scholar

[9]

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer, Heidelberg (1992).

Crossref

Google Scholar

[10]

O'Neill, K.R., Halpern, J.Y.: Secrecy in multiagent systems. CoRR, cs.CR/0307057 (2003).

Crossref

Google Scholar

[11]

Tiplea, F.L., Enea, C.: Abstractions of data types. Acta Informatica 42(8-9), 639- 671 (2006).

Google Scholar

Cited By

View all

Zhou CSun BLiu Z(2018)Abstraction for model checking multi-agent systemsFrontiers of Computer Science in China10.1007/s11704-010-0358-y5:1(14-25)Online publication date: 11-Dec-2018
https://dl.acm.org/doi/10.1007/s11704-010-0358-y
Lomuscio AMichliszyn JJonker CMarsella SThangarajah JTuyls K(2016)Verification of Multi-Agent Systems via Predicate Abstraction against ATLK SpecificationsProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937022(662-670)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937022
Lomuscio AMichaliszyn JWeiss GYolum PBordini RElkind E(2015)Verifying Multi-Agent Systems by Model Checking Three-valued AbstractionsProceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems10.5555/2772879.2772907(189-198)Online publication date: 4-May-2015
https://dl.acm.org/doi/10.5555/2772879.2772907
Show More Cited By

Abstractions of Multi-agent Systems
1. Theory of computation

Recommendations

Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions
AAMAS '15: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems

We develop the theoretical foundations of a predicate abstraction methodology for the verification of multi-agent systems. We put forward a specification language based on epistemic logic and a weak variant of the logic ATL interpreted on a three-valued ...
Truthful monadic abstractions
IJCAR'12: Proceedings of the 6th international joint conference on Automated Reasoning

In intuitionistic sequent calculi, detecting that a sequent is unprovable is often used to direct proof search. This is for instance seen in backward chaining, where an unprovable subgoal means that the proof search must backtrack. In undecidable logics,...
Metareasoning for multi-agent epistemic logics
CLIMA'04: Proceedings of the 5th international conference on Computational Logic in Multi-Agent Systems

We present an encoding of a sequent calculus for a multiagent epistemic logic in Athena, an interactive theorem proving system for many-sorted first-order logic. We then use Athena as a metalanguage in order to reason about the multi-agent logic an as ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CEEMAS '07: Proceedings of the 5th international Central and Eastern European conference on Multi-Agent Systems and Applications V

September 2007

348 pages

ISBN:9783540752530

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 September 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Zhou CSun BLiu Z(2018)Abstraction for model checking multi-agent systemsFrontiers of Computer Science in China10.1007/s11704-010-0358-y5:1(14-25)Online publication date: 11-Dec-2018
https://dl.acm.org/doi/10.1007/s11704-010-0358-y
Lomuscio AMichliszyn JJonker CMarsella SThangarajah JTuyls K(2016)Verification of Multi-Agent Systems via Predicate Abstraction against ATLK SpecificationsProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937022(662-670)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937022
Lomuscio AMichaliszyn JWeiss GYolum PBordini RElkind E(2015)Verifying Multi-Agent Systems by Model Checking Three-valued AbstractionsProceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems10.5555/2772879.2772907(189-198)Online publication date: 4-May-2015
https://dl.acm.org/doi/10.5555/2772879.2772907
Köster MLohmann PSonenberg LStone PTumer KYolum P(2011)Abstraction for model checking modular interpreted systems over ATLThe 10th International Conference on Autonomous Agents and Multiagent Systems - Volume 310.5555/2034396.2034452(1129-1130)Online publication date: 2-May-2011
https://dl.acm.org/doi/10.5555/2034396.2034452
Köster MLohmann P(2011)Abstraction for model checking modular interpreted systems over ATLProceedings of the 9th international conference on Programming Multi-Agent Systems10.1007/978-3-642-31915-0_6(95-113)Online publication date: 3-May-2011
https://dl.acm.org/doi/10.1007/978-3-642-31915-0_6
Lomuscio AQu HRusso F(2010)Automatic data-abstraction in model checking multi-agent systemsProceedings of the 6th international conference on Model checking and artificial intelligence10.5555/2008298.2008302(52-68)Online publication date: 11-Jul-2010
https://dl.acm.org/doi/10.5555/2008298.2008302
Zhou CSun BLiu Z(2010)Abstraction for model checking the probabilistic temporal logic of knowledgeProceedings of the 2010 international conference on Artificial intelligence and computational intelligence: Part I10.5555/1927730.1927764(209-221)Online publication date: 23-Oct-2010
https://dl.acm.org/doi/10.5555/1927730.1927764
Cohen MDam MLomuscio AQu H(2009)A symmetry reduction technique for model checking temporal-epistemic logicProceedings of the 21st International Joint Conference on Artificial Intelligence10.5555/1661445.1661560(721-726)Online publication date: 11-Jul-2009
https://dl.acm.org/doi/10.5555/1661445.1661560
Cohen MDam MLomuscio ARusso FSierra CCastelfranchi CDecker KSichman J(2009)Abstraction in model checking multi-agent systemsProceedings of The 8th International Conference on Autonomous Agents and Multiagent Systems - Volume 210.5555/1558109.1558144(945-952)Online publication date: 10-May-2009
https://dl.acm.org/doi/10.5555/1558109.1558144
Cohen MDam MLomuscio AQu H(2009)A Data Symmetry Reduction Technique for Temporal-epistemic LogicAutomated Technology for Verification and Analysis10.1007/978-3-642-04761-9_6(69-83)Online publication date: 14-Oct-2009
https://dl.acm.org/doi/10.1007/978-3-642-04761-9_6

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Recommendations

Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions

Truthful monadic abstractions

Metareasoning for multi-agent epistemic logics

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations