Article

Model checking for multivalued logic of knowledge and time

Authors:

Beata Konikowska,

Wojciech PenczekAuthors Info & Claims

AAMAS '06: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems

Pages 169 - 176

https://doi.org/10.1145/1160633.1160661

Published: 08 May 2006 Publication History

Abstract

We present a multivalued μK-calculus, an expressive logic to specify knowledge and time in multi-agent systems. We show that the general method of translation [22] from multivalued to two-valued De Morgan algebras can be extended to mv μK-calculus model checking. This way can we reduce the model checking problem for mv μK-calculus to several instances of the model checking problem for two-valued μK-calculus. As a result, properties involving mv μK-calculus or its subsets, like mv CTLK or mv CTL*K, can be verified using any of the available model checking algorithms. Three simple examples are shown to exemplify possible applications of multivalued logics of knowledge and time.

References

[1]

G. Bruns and P. Godefroid. Generalized model checking: Reasoning about partial state spaces. In Proc. of the 11th Int. Conf. on Concurrency Theory (CONCUR'00), volume 1877 of LNCS, pages 168--182. Springer-Verlag, 2000.]]

Digital Library

[2]

G. Bruns and P. Godefroid. Model checking with multi-valued logics. In ICALP, pages 281--293, 2004.]]

[3]

M. Chechik, B. Devereux, and S. Easterbrook. Implementing a multi-valued symbolic model checker. In Proc. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), volume 2031 of LNCS, pages 404--419. Springer-Verlag, 2001.]]

Digital Library

[4]

E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.]]

Digital Library

[5]

S. Easterbrook and M. Chechik. A framework for multi-valued reasoning over inconsistent viewpoints. In Proc. of the 23rd Int. Conf. on Software Engineering (ICSE'01), pages 411--420. IEEE Computer Society, 2001.]]

Digital Library

[6]

R. Fagin, J. Y. Halpern, Y. Moses, and M. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.]]

Digital Library

[7]

M. Fitting. Many-valued modal logics. Fundamenta Informaticae, 15(3--4):335--350, 1991.]]

Digital Library

[8]

M. Fitting. Many-valued modal logics II. Fundamenta Informaticae, 17:55--73, 1992.]]

Digital Library

[9]

P. Godefroid, M. Huth, and R. Jagadeesan. Abstraction-based model checking using modal transition systems. In Proc. of the 12th Int. Conf. on Concurrency Theory (CONCUR'01), volume 2154 of LNCS, pages 426--440. Springer-Verlag, 2001.]]

Digital Library

[10]

P. Godefroid and R. Jagadeesan. On the expressiveness of 3-valued models. In Proc. of the 4th Int. Conf. on Verification, Model Checkig, and Abstract Interpretation (VMCAI'03), volume 2575 of LNCS, pages 206--222. Springer-Verlag, 2003.]]

Digital Library

[11]

A. Gurfinkel and M. Chechik. Multi-valued model checking via classical model checking. In Proc. of the 14th Int. Conf. on Concurrency Theory (CONCUR'03), volume 2761 of LNCS, pages 266--280. Springer-Verlag, 2003.]]

[12]

W. Hoek and M. Wooldridge. Model checking knowledge and time. In Proc. of the 1st Int. SPIN Workshop (SPIN'02), volume 2318 of LNCS, pages 95--111. Springer-Verlag, 2002.]]

Digital Library

[13]

W. Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals. In Proc. of the 1st Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'02), volume III, pages 1167--1174. ACM, July 2002.]]

Digital Library

[14]

M. Huth, R. Jagadeesan, and D. A. Schmidt. A domain equation for refinement of partial systems. Mathematical Structures in Computer Science, 14:469--505, 2004.]]

Digital Library

[15]

M. Huth and S. Pradhan. Consistent partial model checking. In Proc. of the Workshop on Domains VI, volume 73 of ENTCS, pages 45--85. Elsevier, 2004.]]

Digital Library

[16]

W. Jamroga and W. Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2--3):185--219, 2004.]]

Digital Library

[17]

M. Kacprzak, A. Lomuscio, and W. Penczek. From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2--3):221--240, 2004.]]

Digital Library

[18]

M. Kacprzak, A. Lomuscio, and W. Penczek. Verification of multi-agent systems via unbounded model checking. In Proc. of the 3rd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'04), volume II, pages 638--645. IEEE Computer Society, July 2004.]]

Digital Library

[19]

M. Kacprzak and W. Penczek. Unbounded model checking for alternating-time temporal logic. In Proc. of the 3rd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'04), volume II, pages 646--653. IEEE Computer Society, July 2004.]]

Digital Library

[20]

M. Kacprzak and W. Penczek. Fully symbolic unbounded model checking for alternating-time temporal logic. Autonomous Agents and Multi-Agent Systems, 11(1):69--89, 2005.]]

Digital Library

[21]

B. Konikowska and W. Penczek. Model checking multi-valued modal μ-calculus revisited. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'04), volume 170(2) of Informatik-Berichte, pages 307--318.]]

[22]

B. Konikowska and W. Penczek. Model checking for multi-valued computation tree logics. In M. Fitting and E. Orlowska, editors, Beyond Two: Theory and Applications of Multiple Valued Logic, pages 193--210. Physica-Verlag, 2003.]]

Digital Library

[23]

A. Lomuscio, T. Lasica, and W. Penczek. Bounded model checking for interpreted systems: Preliminary experimental results. In Proc. of the 2nd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS'02), volume 2699 of LNAI, pages 115--125. Springer-Verlag, 2003.]]

[24]

R. Meyden and N. V. Shilov. Model checking knowledge and time in systems with perfect recall. In Proc. of the 19th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'99), volume 1738 of LNCS, pages 432--445. Springer-Verlag, 1999.]]

Digital Library

[25]

W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167--185, 2003.]]

Digital Library

[26]

F. Raimondi and A. Lomuscio. A tool for specification and verification of epistemic properties of interpreted systems. In Proc. of the Int. Workshop on Logic and Communication in Multi-Agent Systems (LCMAS'03), volume 85(2) of ENTCS. Elsevier, 2003.]]

[27]

F. Raimondi and A. Lomuscio. Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation. In Proc. of the 3rd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'04), volume II, pages 630--637. IEEE Computer Society, July 2004.]]

Digital Library

[28]

F. Raimondi and A. Lomuscio. Symbolic model checking of multi-agent systems using OBDDs. In Proc. of the 3rd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS III), volume 3228 of LNCS, pages 213--221. Springer-Verlag, 2005.]]

Digital Library

[29]

A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285--309, 1955.]]

[30]

M. Wooldridge. An Introduction to Multiagent Systems. John Wiley & Sons, 2002.]]

Digital Library

[31]

B. Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for deontic interpreted systems. Electr. Notes Theor. Comput. Sci., 126:93--114, 2005.]]

Digital Library

[32]

B. Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for knowledge and real time. In 'Proc. of the 4th Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS'05), pages 165--172. IEEE Computer Society, 2005.]]

Digital Library

Cited By

Baharloo NBentahar JAlwhishi GDrawel NPedrycz W(2024)Verifying trust over IoT-ad hoc network-based applications under uncertaintyAd Hoc Networks10.1016/j.adhoc.2023.103380154(103380)Online publication date: Mar-2024
https://doi.org/10.1016/j.adhoc.2023.103380
Alwhishi GBentahar JElwhishi A(2022)Three-Valued Model Checking Smart Contract Systems with Trust Under UncertaintyThe International Conference on Deep Learning, Big Data and Blockchain (DBB 2022)10.1007/978-3-031-16035-6_10(119-133)Online publication date: 1-Sep-2022
https://doi.org/10.1007/978-3-031-16035-6_10
Belardinelli FLomuscio ALarson KWinikoff MDas SDurfee E(2017)Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect InformationProceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems10.5555/3091125.3091300(1259-1267)Online publication date: 8-May-2017
https://dl.acm.org/doi/10.5555/3091125.3091300
Show More Cited By

Recommendations

Towards model checking interpreted systems
AAMAS '03: Proceedings of the second international joint conference on Autonomous agents and multiagent systems

We show how it is possible to pair the NuSMV model checker with Akka, a software platform used to check validity of propositional modal formulas, to verify static properties of multi-agent systems formalised on interpreted systems semantics.
Model checking epistemic-probabilistic logic using probabilistic interpreted systems

Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. ...
Bounded model checking for knowledge and real time
AAMAS '05: Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems

We present TECTLK, a logic to specify knowledge and real time in multi-agent systems. We show that the model checking problem is decidable, and we present an algorithm for TECTLK bounded model checking based on a discretisation method. We exemplify the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

AAMAS '06: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems

May 2006

1631 pages

ISBN:1595933034

DOI:10.1145/1160633

General Chairs:
Hideyuki Nakashima
Future University - Hakodate, Japan
,
Michael Wellman
University of Michigan
,
Program Chairs:
Gerhard Weiss
Technical University Munich, Germany
,
Peter Stone
The University of Texas at Austin

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

IFMAS: The International Foundation for Multiagent Systems
SIGAI: ACM Special Interest Group on Artificial Intelligence
ATAL: The International Workshop on Agent Theories, Architectures, and Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 May 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

AAMAS06

Sponsor:

IFMAS
SIGAI
ATAL

AAMAS06: AAMAS '06 - 5th International Joint Conference on Autonomous Agents and Multi-agent Systems 2006

May 8 - 12, 2006

Japan, Hakodate

Acceptance Rates

Overall Acceptance Rate 1,155 of 5,036 submissions, 23%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
287
Total Downloads

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

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Baharloo NBentahar JAlwhishi GDrawel NPedrycz W(2024)Verifying trust over IoT-ad hoc network-based applications under uncertaintyAd Hoc Networks10.1016/j.adhoc.2023.103380154(103380)Online publication date: Mar-2024
https://doi.org/10.1016/j.adhoc.2023.103380
Alwhishi GBentahar JElwhishi A(2022)Three-Valued Model Checking Smart Contract Systems with Trust Under UncertaintyThe International Conference on Deep Learning, Big Data and Blockchain (DBB 2022)10.1007/978-3-031-16035-6_10(119-133)Online publication date: 1-Sep-2022
https://doi.org/10.1007/978-3-031-16035-6_10
Belardinelli FLomuscio ALarson KWinikoff MDas SDurfee E(2017)Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect InformationProceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems10.5555/3091125.3091300(1259-1267)Online publication date: 8-May-2017
https://dl.acm.org/doi/10.5555/3091125.3091300
Jamroga WKonikowska BPenczek WJonker CMarsella SThangarajah JTuyls K(2016)Multi-Valued Verification of Strategic AbilityProceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems10.5555/2936924.2937097(1180-1189)Online publication date: 9-May-2016
https://dl.acm.org/doi/10.5555/2936924.2937097
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
Kamide N(2012)Reasoning about time-dependent multi-agentsTransactions on Compuational Collective Intelligence VI10.1007/978-3-642-29356-6_9(181-201)Online publication date: 1-Jan-2012
https://dl.acm.org/doi/10.1007/978-3-642-29356-6_9
Enea CDima C(2007)Abstractions of Multi-agent SystemsProceedings of the 5th international Central and Eastern European conference on Multi-Agent Systems and Applications V10.1007/978-3-540-75254-7_2(11-21)Online publication date: 25-Sep-2007
https://dl.acm.org/doi/10.1007/978-3-540-75254-7_2
Cao Z(2007)Representing and Verifying Temporal Epistemic Properties in Multi-Agent SystemsComputational Logic in Multi-Agent Systems10.1007/978-3-540-69619-3_8(134-150)Online publication date: 2007
https://doi.org/10.1007/978-3-540-69619-3_8
Cao Z(2006)Representing and verifying temporal epistemic properties in multi-agent systemsProceedings of the 7th international conference on Computational logic in multi-agent systems10.5555/1758663.1758672(134-150)Online publication date: 8-May-2006
https://dl.acm.org/doi/10.5555/1758663.1758672

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents