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 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