Abstract Artificial ants are “small” units, moving autonomously on a shared, dynamically changing “space”, directly or indirectly exchanging some kind of information. Artificial ants are frequently conceived as a paradigm for collective adaptive systems. In this paper, we discuss means to represent continuous moves of “ants” in discrete models. More generally, we challenge the role of the notion of “time” in artificial ant systems and models. We suggest a modeling framework that structures behavior along causal dependencies rather than temporal relations. We present all arguments with the help of a simple example. As a modeling framework we employ Heraklit; an emerging framework that has already proven its worth in many contexts. Different concrete collective systems share similar features, despite differences in the size of basic sets, concrete values of functions, etc., and can therefore be conceived as instantiations of a single schema. Hence, we need a representation of systems on the schematic level.

Abstract Cuneiform is a minimal functional programming language for large-scale scientific data analysis. Implementing a strict black-box view on external operators and data, it allows the direct embedding of code in a variety of external languages like Python or R, provides data-parallel higher order operators for processing large partitioned data sets, allows conditionals and general recursion, and has a naturally parallelizable evaluation strategy suitable for multi-core servers and distributed execution environments like Hadoop, HTCondor, or distributed Erlang. Cuneiform has been applied in several data-intensive research areas including remote sensing, machine learning, and bioinformatics, all of which critically depend on the flexible assembly of pre-existing tools and libraries written in different languages into complex pipelines. This paper introduces the computation semantics for Cuneiform. It presents Cuneiform's abstract syntax, a simple type system, and the semantics of evaluation. Providing an unambiguous specification of the behavior of Cuneiform eases the implementation of interpreters which we showcase by providing a concise reference implementation in Erlang. The similarity of Cuneiform's syntax to the simply typed lambda calculus puts Cuneiform in perspective and allows a straightforward discussion of its design in the context of functional programming. Moreover, the simple type system allows the deduction of the language's safety up to black-box operators. Last, the formulation of the semantics also permits the verification of compilers to and from other workflow languages.

The paradigm of Service-Oriented Computing (SOC) provides a framework for interorganizational business processes and for the emerging programming-in-the-large. The basic idea of SOC, the interaction of services, rises a lot of issues such as proper termination of interacting services or substitution of a service by another one. Such issues can be addressed by means of models of services. We show how services can intelligibly be modeled, and we present algorithms and tools to analyze properties of service models. In order to emphasize that our models properly reflect real world issues of services, we also show that services represented in established languages such as WS-BPEL can be transformed into our formal method.

The temporal logic of distributed actions (TLDA) is a new temporal logic designed for the specification and verification of distributed systems. The logic supports a compositional design of systems: subsystems can be specified separately and then be integrated into one system. TLDA can be syntactically viewed as an extension of TLA. We propose a different semantical model based on partial order which increases the expressiveness of the logic.

An algorithm is said to be distributed if it operates on a physically or logically distributed computing architecture. Typically, such architectures lack global control. This requires particular means to model and to verify distributed algorithms. Distributed algorithms are frequently designed in an abstract setting, assuming any network of agents. One of the agents is frequently assumed to initiate a computation, with all other agents reacting by means of identical algorithms. Each agent is aware of its neighbour agents only. Hence, such an algorithm is a schema of behaviour, to run on any in a whole class of networks, such as the connected networks, the ring-or tree-shaped networks, etc. We suggest a representation technique that is particularly tailored to distributed algorithms, based on the observation that the adequate operational primitives of distributed algorithms include local atomic actions, synchronization, local states, message buffers and similar constructs, whereas assignment: statements and global states are no longer essential. Furthermore, a verification technique is presented, allowing surprisingly simple and transparent proofs. This technique includes well established Petri net based concepts as well as new, temporal logic based arguments. The logic exploits the particularly simple structure of Petri nets: Petri net places are taken as predicates, Petri net transitions are elementary predicate transforms, and the notion of concurrent runs yields means to adequately argue on local progress and phase based behaviour.

Abstract A technique to model and to verify distributed algorithms is suggested. This technique (based on Petri nets) reduces the modelling and analysis effort to a reasonable level. The paper outlines the technique using the example of a typical network algorithm, the echo algorithm .