Abstract
This chapter presents the hybrid Temporal Trace Language (TTL) for formal specification and analysis of dynamic properties of multi-agent systems. This language supports specification of both qualitative and quantitative aspects, and subsumes languages based on differential equations and temporal logics. TTL has a high expressivity and normal forms that enable automated analysis. Software environments for performing verification of TTL specifications have been developed. TTL proved its value in a number of domains.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Kowalski, R., Sergot, M.: A logic-based calculus of events. New Generation Computing 4, 67–95 (2002)
Horling, B., Lesser, V.: A survey of multi-agent organizational paradigms. The Knowledge Engineering Review 19(4), 281–316 (2004)
Fuxman, A., Liu, L., Pistore, M., Roveri, M., Mylopoulos, J.: Specifying and analyzing early requirements in tropos. Requirements Engineering Journal 9(2), 132–150 (2004)
McDermott, D.: A temporal logic for reasoning about processes and plans. Cognitive Science 6, 101–155 (1982)
Bosse, T., Jonker, C., van der Meij, L., Sharpanskykh, A., Treur, J.: Specification and verification of dynamics in agent models. International Journal of Cooperative Information Systems 18(1), 167–193 (2009)
Ferber, J., Gutknecht, O., Michel, F.: From Agents to Organizations: An Organizational View of Multi-agent Systems, vol. 2935, pp. 214–230. Springer (2004)
Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Publishing Company, Amsterdam (1962)
Fitting, M.: First-order Logic and Automated Theorem Proving. MIT Press, Springer Verlag (1996)
Hooman, J.: Compositional verification of a distributed real-time arbitration protocol. Real-Time Systems 6, 173–206 (1994)
Pinto, J., Reiter, R.: Reasoning about time in the situation calculus. Ann. Math. Artif. Intell 14, 251–268 (1995)
Manzano, M.: Extensions of First Order Logic. Cambridge University Press (1996)
Davoren, J., Nerode, A.: Logics for hybrid systems. Proceedings of the IEEE 88(7), 985–1010 (2000)
van Benthem, J.: The Logic of Time: A Model-theoretic Investigation into the Varieties of Temporal Ontology and Temporal Discourse. Reidel, Dordrecht (1983)
Marca, D.: SADT: Structured Analysis and Design Techniques. McGraw-Hill, Cambridge MA (1988)
Goldblatt, R.: Logics of Time and Computation, CSLI Lecture Notes, vol. 7, 2nd edn. Springer (1992)
Port, R., van Gelder, T. (eds.): Mind as Motion: Explorations in the Dynamics of Cognition. MIT Press (1995)
Dignum, V. (ed.): Multi-Agent Systems - Semantics and Dynamics of Organizational Models. IGI Global (2009)
Bosse, T., Gerritsen, C., Treur, J.: Cognitive and social simulation of criminal behaviour: the intermittent explosive disorder case. In: Proceedings of the Sixth International Joint Conference on Autonomous Agents and Multi-Agent Systems, AAMAS’07, pp. 367–374. ACM Press (2007)
Bosse, T., Sharpanskykh, A., Treur, J.: Modelling complex systems by integration of agent-based and dynamical systems models. In: A. Minai, D. Braha, Y. Bar-Yam (eds.) Unifying Themes in Complex Systems VI, Proceedings of the Sixth International Conference on Complex Systems. Springer (2008)
Sharpanskykh, A., Treur, J.: Verifying interlevel relations within multi-agent systems. In: Proceedings of the 17th European Conference on Artificial Intelligence, ECAI’06, pp. 290–294. IOS Press (2006)
Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: Proceedings of the 43rd annual conference on Design automation (DAC ’06) (2006)
Andreka, H., van Benthem, J., Nemeti, I.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic 27, 217–274 (1998)
Treur, J.: Past-future separation and normal forms in temporal predicate logic specifications. Journal of Algorithms in Cognition, Informatics and Logic 64 (2009). Doi http://dx.doi.org/10.1016/j.jalgor.2009.02.008 (in press)
Jonker, C., Treur, J.: Compositional verification of multi-agent systems: a formal analysis of pro-activeness and reactiveness. International Journal of Cooperative Information Systems 11, 51–92 (2002)
Barringer, H., Fisher, M., Gabbay, D., Owens, R., Reynolds, M.: The Imperative Future: Principles of Executable Temporal Logic. John Wiley & Sons (1996)
Cysneiros, L., Yu., E.: Requirements engineering for large-scale multi-agent systems. In: Proceedings of the 1st International Central and Eastern European Conference on Multi-Agent Systems (CEEMAS’02), pp. 39–56. Springer Verlag (2002)
Pearson, C.: Numerical Methods in Engineering and Science. CRC Press (1986)
Reiter, R.: Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. MIT Press, Cambridge, MA (2001)
Purdy, W.: Fluted formulas and the limits of decidability. Journal of Symbolic Logic 61, 608–620 (1996)
Bosse, T., Jonker, C., van der Meij, L., Treur, J.: A language and environment for analysis of dynamics by simulation. International Journal of Artificial Intelligence Tools 16(3), 435–464 (2007)
Manna, Z., Pnueli, A.: Verifying Hybrid Systems, vol. 736, pp. 4–35. Springer (1993)
Bosse, T., Jonker, C., Los, S., van der Torre, L., Treur, J.: Formal analysis of trace conditioning. Cognitive Systems Research Journal 8, 36–47 (2007)
Sharpanskykh, A., Treur, J.: Relating cognitive process models to behavioural models of agents. In: Proceedings of the 8th IEEE/WIC/ACM International Conference on Intelligent Agent Technology, IAT’08, pp. 330–335. IEEE Computer Society Press (2008)
McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers (1993)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)
Mazurkiewicz, A.: Trace Theory, in Advances in Petri nets II: applications and relationships to other models of concurrency, LNCS, vol. 255. Springer (1987)
Jonker, C., Sharpanskykh, A., Treur, J., Yolum, P.: A framework for formal modeling and analysis of organizations. Applied Intelligence 27(1), 49–66 (2007)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media, LLC
About this chapter
Cite this chapter
Sharpanskykh, A., Treur, J. (2010). A Temporal Trace Language for Formal Modelling and Analysis of Agent Systems. In: Dastani, M., Hindriks, K., Meyer, JJ. (eds) Specification and Verification of Multi-agent Systems. Springer, Boston, MA. https://doi.org/10.1007/978-1-4419-6984-2_11
Download citation
DOI: https://doi.org/10.1007/978-1-4419-6984-2_11
Published:
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-6983-5
Online ISBN: 978-1-4419-6984-2
eBook Packages: Computer ScienceComputer Science (R0)