Abstract
The paper deals with symbolic approaches to bounded model checking (BMC) for Linear Time Temporal Logic extended with the epistemic component (LTLK), interpreted over Interleaved Interpreted Systems. Two translations of BMC for LTLK to SAT and to operations on BDDs are presented. The translations have been implemented, tested, and compared with each other as well as with another tool on several benchmarks for MAS. Our experimental results reveal advantages and disadvantages of SAT- versus BDD-based BMC for LTLK. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Mȩski, A., Penczek, W., Szreter, M., Woźna-Szcześniak, B., & Zbrzezny, A. (2012). Two approaches to bounded model checking for linear time logic with knowledge. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7327 LNAI, pp. 514–523). https://doi.org/10.1007/978-3-642-30947-2_56
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
