Cited By
View all- Knapik MMęski APenczek W(2015)Action Synthesis for Branching Time LogicACM Transactions on Embedded Computing Systems10.1145/274633714:4(1-23)Online publication date: 9-Sep-2015
Group synthesis for parametric temporal-epistemic logic
Pages 1107 - 1114
Abstract
We investigate parameter synthesis in the context of temporal-epistemic logic. We introduce CTLPK, a parametric extension to the branching time temporal-epistemic logic CTLK with free variables representing groups of agents. We give algorithms for automatically synthesising the groups of agents that make a given parametric formula satisfied. We discuss an implementation of the technique on top of the open-source model checker mcmas and demonstrate its attractiveness by reporting the experimental results obtained.
References
[1]
D. Chaum. The Dining Cryptographers Problem. J. Cryptol., 1:65--75, 1988.
[2]
E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, USA, 1999.
[3]
J. Ezekiel and A. Lomuscio. A Methodology for Automatic Diagnosability Analysis. In Proc. of ICFEM'10, pages 549--564, 2010.
[4]
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning About Knowledge. MIT Press, 1995.
[5]
P. Gammie and R. van der Meyden. MCK: Model Checking the Logic of Knowledge. In Proc. of CAV'04, pages 479--483, 2004.
[6]
M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning About Systems (Second Edition). Cambridge University Press, 2004.
[7]
M. Kacprzak, W. Nabialek, A. Niewiadomski, W. Penczek, A. Pólrola, M. Szreter, B. Wozna, and A. Zbrzezny. VerICS 2007 - a Model Checker for Knowledge and Real-Time. Fundam. Inform., 85(1-4):313--328, 2008.
[8]
M. Knapik, W. Penczek, M. Szreter, and A. Pólrola. Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics. Fundam. Inform., 101(1-2):9--27, 2010.
[9]
A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In Proc. of CAV'09, pages 682--688, 2009.
[10]
R. v. d. Meyden and K. Su. Symbolic Model Checking the Knowledge of the Dining Cryptographers. In Proc. of CSFW'04, pages 280--291, 2004.
[11]
W. Penczek and A. Lomuscio. Verifying Epistemic Properties of Multi-Agent Systems via Bounded Model Checking. Fundam. Inform., 55(2):167--185, 2003.
[12]
F. Raimondi and A. Lomuscio. Automatic Verification of Multi-Agent Systems by Model Checking via Ordered Binary Decision Diagrams. J. Applied Logic, 5(2):235--251, 2007.
[13]
F. Wang. Timing Behavior Analysis for Real-Time Systems. In Proc. of LICS'95, pages 112--122, 1995.
Index Terms
- Group synthesis for parametric temporal-epistemic logic
Recommendations
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. ...
Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications
In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In ...
A Lazy Approach to Temporal Epistemic Logic Model Checking
AAMAS '16: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent SystemsTemporal Epistemic Logic is used to reason about the evolution of knowledge over time. A notable example is the temporal epistemic logic KL1, which is used to model what a reasoner can infer about the state of a dynamic system by using available ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2012
601 pages
ISBN:0981738125
Sponsors
- The International Foundation for Autonomous Agents and Multiagent Systems: The International Foundation for Autonomous Agents and Multiagent Systems
In-Cooperation
Publisher
International Foundation for Autonomous Agents and Multiagent Systems
Richland, SC
Publication History
Published: 04 June 2012
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
AAMAS 12
Sponsor:
- The International Foundation for Autonomous Agents and Multiagent Systems
AAMAS 12: International Conference on Autonomous Agents and Multiagent Systems
June 4 - 8, 2012
Valencia, Spain
Acceptance Rates
Overall Acceptance Rate 1,155 of 5,036 submissions, 23%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 53Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 23 Nov 2024
Other Metrics
Citations
Cited By
View all- Knapik MMęski APenczek W(2015)Action Synthesis for Branching Time LogicACM Transactions on Embedded Computing Systems10.1145/274633714:4(1-23)Online publication date: 9-Sep-2015
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in