Symbolic Synthesis for Epistemic Specifications with Observational Semantics
作者： Xiaowei Huang , Ron van der Meyden
DOI: 10.1007/978-3-642-54862-8_39
关键词: Theoretical computer science 、 Computer science 、 Epistemic modal logic 、 Reduction (recursion theory) 、 Semantics (computer science) 、 Mutual exclusion 、 Epistemology 、 Observational study 、 Critical section 、 Model checking 、 Program structure
摘要: The paper describes a framework for the synthesis of protocols distributed and multi-agent systems from specifications that give program structure may include variables in place conditional expressions, together with temporal epistemic logic constrain values these variables. operators are interpreted respect to an observational semantics. generalizes notion knowledge-based proposed by Fagin et al (Dist. Comp. 1997). An algorithmic approach problem is developed computes all solutions, using reduction model checking, has been implemented symbolic techniques. application synthesize mutual exclusion presented.
springer.com
sci-hub.st 参考文章(28)
Time for Verification Lecture Notes in Computer Science. ,vol. 6200, ,(2010) , 10.1007/978-3-642-13754-9
Pradip K. Srimani, Sunil R. Lakhani, Distributed mutual exclusion algorithms IEEE Computer Society Press. ,(1992)
Kai Baukus, Ron van der Meyden, A Knowledge Based Analysis of Cache Coherence international conference on formal engineering methods. pp. 99- 114 ,(2004) , 10.1007/978-3-540-30482-1_15
Peter Gammie, Ron van der Meyden, MCK: Model Checking the Logic of Knowledge Computer Aided Verification. ,vol. 3114, pp. 479- 483 ,(2004) , 10.1007/978-3-540-27813-9_41
Ron van der Meyden, Thomas Wilke, Synthesis of Distributed Systems from Knowledge-Based Specifications Lecture Notes in Computer Science. pp. 562- 576 ,(2005) , 10.1007/11539452_42
Ron van der Meyden, Yoram Moses, Kai Engelhardt, Knowledge and the logic of local propositions theoretical aspects of rationality and knowledge. pp. 29- 41 ,(1998)
Saddek Bensalem, Doron Peled, Joseph Sifakis, Knowledge based scheduling of distributed systems Lecture Notes in Computer Science. ,vol. 6200, pp. 26- 41 ,(2010) , 10.1007/978-3-642-13754-9_2
Moshe Y. Vardi, Implementing knowledge-based programs theoretical aspects of rationality and knowledge. pp. 15- 30 ,(1996)
Alessio Lomuscio, Hongyang Qu, Franco Raimondi, MCMAS: A Model Checker for the Verification of Multi-Agent Systems Computer Aided Verification. pp. 682- 688 ,(2009) , 10.1007/978-3-642-02658-4_55
Yoah Bar-David, Gadi Taubenfeld, Automatic Discovery of Mutual Exclusion Algorithms international symposium on distributed computing. pp. 136- 150 ,(2003) , 10.1007/978-3-540-39989-6_10