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

Nadeem Akhtar, Muhammad Nauman

Department of Computer Science and IT, The Islamia University of Bahawalpur, Baghdad-ul-Jadeed Campus, Bahawalpur, Pakistan.

DOI: 10.4236/jsea.2015.82006                

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.

Keywords

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

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	George, V. and Vaughn, R. (2003) Application of Lightweight Formal Methods in Requirement Engineering. Crosstalk: The Journal of Defense Software Engineering, 16, 30.
[2]	Wooldridge, M. (2002) An Introduction to MultiAgent Systems. John Wiley and Sons, Chichester.
[3]	Wooldridge, M., Jennings, N.R. and Kinny, D. (2000) The Gaia Methodology for Agent-Oriented Analysis and Design. Autonomous Agents and Multi-Agent Systems, 3, 285-312. http://dx.doi.org/10.1023/A:1010071910869
[4]	Dogac, A. and Cingil, I. (2004) Agent Technology. In: B2B E-Commerce Technology: Frameworks, Standards and Emerging Issues, Addison-Wesley, Boston, 103-150.
[5]	Wooldridge, M. and Jennings, N.R. (1995) Intelligent Agents: Theory and Practice. The Knowledge Engineering Review, 10, 115-152. http://dx.doi.org/10.1017/S0269888900008122
[6]	Weyns, D., Omicini, A. and Odell, J. (2007) Environment as a First-Class Abstraction in Multi-Agent Systems. International Journal of Autonomous Agents and Multi-Agent Systems, 14, 5-30.
[7]	Russell, S. and Norvig, P. (2002) Artificial Intelligence: A Modern Approach. 2nd Edition, Prentice Hall, Upper Saddle River.
[8]	Demazeau, Y. (2003) Multi-Agent Systems Methodology. Franco-Mexican School on Cooperative and Distributed Systems (LAFMI).
[9]	Ferber, J. (1999) An Introduction to Distributed Artificial Intelligence. Addison-Wesley, Boston.
[10]	Jennings, N.R., Sycara, K. and Wooldridge, M. (1998) A Roadmap of Agent Research and Develo-pment. International Autonomous Agents and Multi-Agent Systems, 1, 7-38. http://dx.doi.org/10.1023/A:1010090405266
[11]	Ghezzi, C., Jazayeri, M. and Mandrioli, D. (2003) Fundamentals of Software Engineering. 2nd Edition, Prentice Hall, Upper Saddle River.
[12]	Magee, J. and Kramer, J. (2006) Concurrency: State Models and Java Programs. 2nd Edition, John Wiley and Sons, Hoboken.
[13]	Giannakopoulou, D., Magee, J. and Kramer, J. (1999) Fairness and Priority in Progress Property Analysis. Technical report, Department of Computing, Imperial College of Science, Technology and Medicine, London.
[14]	Clarke, E.M. and Emerson, E.A. (1981) Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. In: Kozen, D., Ed., Logics of Programs, Volume 131, Springer-Verlag, New York, 52-71.
[15]	Quielle, J.P. and Sifakis, J. (1982) Specification and Verification of Concurrent Systems in CESAR. Proceedings of the 5th International Symposium on Programming, Turin, 6-8 April 1982, 337-351. http://dx.doi.org/10.1007/3-540-11494-7_22
[16]	Clarke, E., Grumberg, O. and Peled, D. (1999) Model Checking. MIT Press, Cambridge.
[17]	Clarke, E.M., Emerson, E.A. and Sistla, A.P. (1986) Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8, 244-263.
[18]	Clarke, E.M., Grumberg, O. and Long, D.E. (1994) Model Checking and Abstraction. ACM Transactions on Programming Languages and Systems, 16, 1512-1542. http://dx.doi.org/10.1145/186025.186051
[19]	Clarke, E.M., Grumberg, O., Jha, S., Lu, Y. and Veith, H. (2003) Counter Example-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM, 50, 752-794. http://dx.doi.org/10.1145/876638.876643
[20]	Larsen, K.G., Pettersson, P. and Yi, W. (1997) UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer, 1, 134-152.
[21]	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.