References

  1. R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani & S. Tasiran (1998): MOCHA: Modularity in model checking. In: Alan Hu & Moshe Vardi: Computer Aided Verification, Lecture Notes in Computer Science 1427. Springer Berlin / Heidelberg, pp. 521–525, doi:10.1007/BFb0028774.
  2. F. Buccafurri, T. Eiter, G. Gottlob & N. Leone (2001): On ACTL Formulas Having Linear Counterexamples. Journal of Computer and System Sciences 62(3), pp. 463 – 515, doi:10.1006/jcss.2000.1734.
  3. D. Chaum (1988): The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1, pp. 65–75, doi:10.1007/BF00206326.
  4. A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani & A. Tacchella (2002): NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Ed Brinksma & Kim Larsen: Computer Aided Verification, Lecture Notes in Computer Science 2404. Springer Berlin / Heidelberg, pp. 241–268, doi:10.1007/3-540-45657-0_29.
  5. E. M. Clarke & E. A. Emerson (1982): Design and synthesis of synchronization skeletons using branching time temporal logic. In: Dexter Kozen: Logics of Programs, Lecture Notes in Computer Science 131. Springer Berlin / Heidelberg, pp. 52–71, doi:10.1007/BFb0025774.
  6. E. M. Clarke, O. Grumberg & D. Peled (1999): Model Checking. MIT Press.
  7. E. M. Clarke, S. Jha, Y. Lu & H. Veith (2002): Tree-Like Counterexamples in Model Checking. In: Proc. of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 19–29, doi:10.1109/LICS.2002.1029814.
  8. F. Copty, A. Irron, O. Weissberg, N. Kropp & G. Kamhi (2003): Efficient debugging in a formal verification environment. International Journal on Software Tools for Technology Transfer (STTT) 4, pp. 335–348, doi:10.1007/s10009-002-0097-y.
  9. Y. Dong, C. R. Ramakrishnan & S. A. Smolka (2003): Model Checking and Evidence Exploration. In: Proc. of the 10th IEEE International Conference on Engineering of Computer-Based Systems (ECBS 2003), pp. 214–223, doi:10.1109/ECBS.2003.1194802.
  10. P. Gammie & R. van der Meyden (2004): MCK: Model Checking the Logic of Knowledge. In: Proceedings of 16th International Conference on Computer Aided Verification (CAV'04), LNCS 3114. Springer-Verlag, pp. 479–483, doi:10.1007/978-3-540-27813-9_41.
  11. A. Groce & W. Visser (2003): What Went Wrong: Explaining Counterexamples. In: Thomas Ball & Sriram Rajamani: Model Checking Software, Lecture Notes in Computer Science 2648. Springer Berlin / Heidelberg, pp. 121–136, doi:10.1007/3-540-44829-2_8.
  12. A. Gurfinkel & M. Chechik (2003): Proof-Like Counter-Examples. In: Hubert Garavel & John Hatcliff: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 2619. Springer Berlin / Heidelberg, pp. 160–175, doi:10.1007/3-540-36577-X_12.
  13. H. S. Jin, K. Ravi & F. Somenzi (2004): Fate and free will in error traces. International Journal on Software Tools for Technology Transfer (STTT) 6, pp. 102–116, doi:10.1007/s10009-004-0146-9.
  14. A. Lomuscio, C. Pecheur & F. Raimondi (2007): Automatic Verification of Knowledge and Time with NuSMV. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 1384–1389. Available at http://hdl.handle.net/2078.1/79759.
  15. A. Lomuscio & F. Raimondi (2006): MCMAS: A Model Checker for Multi-agent Systems. In: Holger Hermanns & Jens Palsberg: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 3920. Springer Berlin / Heidelberg, pp. 450–454, doi:10.1007/11691372_31.
  16. R. Meolic, A. Fantechi & S. Gnesi (2004): Witness and Counterexample Automata for ACTL. In: David de Frutos-Escrig & Manuel Núñez: Formal Techniques for Networked and Distributed Systems – FORTE 2004, Lecture Notes in Computer Science 3235. Springer Berlin / Heidelberg, pp. 259–275, doi:10.1007/978-3-540-30232-2_17.
  17. C. Pecheur & F. Raimondi (2007): Symbolic Model Checking of Logics with Actions. In: Stefan Edelkamp & Alessio Lomuscio: Model Checking and Artificial Intelligence, Lecture Notes in Computer Science 4428. Springer Berlin / Heidelberg, pp. 113–128, doi:10.1007/978-3-540-74128-2_8.
  18. W. Penczek & A. Lomuscio (2003): Verifying Epistemic Properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), pp. 167–185, doi:10.1145/860606.860609.
  19. W. Penczek, B. Wozna & A. Zbrzezny (2002): Bounded Model Checking for the Universal Fragment of CTL. Fundam. Inform. 51(1-2), pp. 135–156. Available at http://iospress.metapress.com/content/p4dgu2g0tqgtyh4b/.
  20. A. Rasse (1992): Error diagnosis in finite communicating systems. In: Kim Larsen & Arne Skou: Computer Aided Verification, Lecture Notes in Computer Science 575. Springer Berlin / Heidelberg, pp. 114–124, doi:10.1007/3-540-55179-4_12.
  21. S. Shoham & O. Grumberg (2003): A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. In: Rebecca Wright: Financial Cryptography, Lecture Notes in Computer Science 2742. Springer Berlin / Heidelberg, pp. 275–287, doi:10.1007/978-3-540-45069-6_28.
  22. P. Stevens & C. Stirling (1998): Practical model-checking using games. In: Bernhard Steffen: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1384. Springer Berlin / Heidelberg, pp. 85–101, doi:10.1007/BFb0054166.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org