Katoen, J.P. (1999) Concepts, Algorithms, and Tools for Model Checking. A Lecture Notes of the Course Mechanized Validation of Parallel Systems. For 1998/99 at Friedrich-Alexander Universitat, Erlangen-Nurnberg, 195.

has been cited by the following article:

• TITLE: Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study

  AUTHORS: Nadeem Akhtar, Muhammad Nauman

  KEYWORDS: Software Correctness, Formal Verification, Model Checking, Timed-Automata, Multi-Agent System, Timed Computation Tree Logic (TCTL)

  JOURNAL NAME: Journal of Software Engineering and Applications, Vol.8 No.2, February 12, 2015

  ABSTRACT: A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.