On the needs for specification and verification of collaborative and concurrent robots, agents and processes

  • This report summarises and integrates two different tracks of research for the purpose of envisioning and preparing a joint research project proposal. Soft- and hardware systems have become increasingly complex and act "concurrently", both with respect to memory access (i.e. information flow) and computational resources (i.e. "services"). The software development metaphor of cloud-storage, cloud-computing and service-oriented design has been anticipated by artificial intelligence (AI) research at least 30 years ago (parallel and distributed computation already dates back to the 1950’s and 1970s). What is known as a "service" today is what in AI is known as the capability of an agent; and the problem of information flow and consistency has been a headstone of information processing ever since. Based on a real-world robotics application we demonstrate how an increasingly abstract description of collaborating or competing agents correspond to a set of concurrent processes. In the secondThis report summarises and integrates two different tracks of research for the purpose of envisioning and preparing a joint research project proposal. Soft- and hardware systems have become increasingly complex and act "concurrently", both with respect to memory access (i.e. information flow) and computational resources (i.e. "services"). The software development metaphor of cloud-storage, cloud-computing and service-oriented design has been anticipated by artificial intelligence (AI) research at least 30 years ago (parallel and distributed computation already dates back to the 1950’s and 1970s). What is known as a "service" today is what in AI is known as the capability of an agent; and the problem of information flow and consistency has been a headstone of information processing ever since. Based on a real-world robotics application we demonstrate how an increasingly abstract description of collaborating or competing agents correspond to a set of concurrent processes. In the second part we review several approaches to the theory of concurrent systems. Based on the different kinds of program semantics we present corresponding logical and algebraic means for the description of parallel processes and memory access. It turns out that Concurrent Kleene Algebra (CKA) and its related graphlet metaphor appears to deliver a one-to-one matching formal description of the module structures developed in the first part. The problem of snapshotting system states in order to receive (partial) traces of a running system seems to be well describable by a Temporal Logic of Actions (TLA). Finally, the different types of subsystems and their mutual requirements such as exclusiveness etc. seem to be best describable in a separation-logic like approach. We conclude with a list of research questions detailing some of the many promising issues raised in the report.show moreshow less

Download full text files

Export metadata

Statistics

Number of document requests

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Martin E. MüllerORCiDGND
URN:urn:nbn:de:bvb:384-opus4-34066
Frontdoor URLhttps://opus.bibliothek.uni-augsburg.de/opus4/3406
Series (Serial Number):Reports / Technische Berichte der Fakultät für Angewandte Informatik der Universität Augsburg (2015-03)
Type:Report
Language:English
Publishing Institution:Universität Augsburg
Release Date:2016/01/05
Institutes:Fakultät für Angewandte Informatik
Fakultät für Angewandte Informatik / Institut für Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):Deutsches Urheberrecht mit Print on Demand