Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
作者： Alessio Lomuscio , Wojciech Penczek
DOI:
关键词:
摘要: This article surveys some of the recent work in verification temporal epistemic logic via symbolic model checking, focusing on OBDD-based and SAT-based approaches for logics built discrete real-time branching time logics.
arxiv.org
harvard.edu参考文章(55)
M. Kacprzak, Alessio Lomuscio, Wojciech Penczek, Unbounded Model Checking for Knowledge and Time Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk. pp. 1- 27 ,(2003)
Wolfgang Lenzen, Recent work in epistemic logic ,(1978)
Franco Raimondi, Model checking multi-agent systems Doctoral thesis, University of London.. ,(2006)
A. Lomuscio, M. Kacprzak, W. Penczek, From Bounded to Unbounded Model Checking for Temporal Epistemic Logic Fundamenta Informaticae. ,vol. 63, pp. 221- 240 ,(2004)
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
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
Wiebe van der Hoek, Michael Wooldridge, Model Checking Knowledge and Time international workshop on model checking software. pp. 95- 111 ,(2002) , 10.1007/3-540-46017-9_9
E. M. Clarke, Daniel Kroening, Pankaj Chauhan, Using SAT based image computation for reachability analysis ,(2003)
M.K. Ganai, A. Gupta, P. Ashar, Efficient SAT-based unbounded symbolic model checking using circuit cofactoring international conference on computer aided design. pp. 510- 517 ,(2004) , 10.1109/ICCAD.2004.1382631
Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem Ph. D. Thesis, Carnegie Mellon University. ,(1992)