Field-based coordination has been proposed as a model for coordinating collective adaptive systems, promoting a view of distributed computations as functions manipulating data structures spread over space and evolving over time, called computational fields. The field calculus is a formal foundation for field computations, providing specific constructs for evolution (time) and neighbor interaction (space), which are handled by separate operators (called rep and nbr, respectively). This approach, however, intrinsically limits the speed of information propagation that can be achieved by their combined use. In this paper, we propose a new field-based coordination operator called share, which captures the space-time nature of field computations in a single operator that declaratively achieves: (i) observation of neighbors' values; (ii) reduction to a single local value; and (iii) update and converse sharing to neighbors of a local variable. We show that for an important class of self-stabilising computations, share can replace all occurrences of rep and nbr constructs. In addition to conceptual economy, use of the share operator also allows many prior field calculus algorithms to be greatly accelerated, which we validate empirically with simulations of frequently used network propagation and collection algorithms.

In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabilistic programming languages, not much has been done to combine those two approaches. In this paper, we initiate a study on the probabilistic higher-order model checking problem, by giving some first theoretical and experimental results. As a first step towards our goal, we introduce PHORS, a probabilistic extension of higher-order recursion schemes (HORS), as a model of probabilistic higher-order programs. The model of PHORS may alternatively be viewed as a higher-order extension of recursive Markov chains. We then investigate the probabilistic termination problem -- or, equivalently, the probabilistic reachability problem. We prove that almost sure termination of order-2 PHORS is undecidable. We also provide a fixpoint characterization of the termination probability of PHORS, and develop a sound (but possibly incomplete) procedure for approximately computing the termination probability. We have implemented the procedure for order-2 PHORSs, and confirmed that the procedure works well through preliminary experiments that are reported at the end of the article.

We introduce a framework for approximate analysis of Markov decision processes (MDP) with bounded-, unbounded-, and infinite-horizon properties. The main idea is to identify a "core" of an MDP, i.e., a subsystem where we provably remain with high probability, and to avoid computation on the less relevant rest of the state space. Although we identify the core using simulations and statistical techniques, it allows for rigorous error bounds in the analysis. Consequently, we obtain efficient analysis algorithms based on partial exploration for various settings, including the challenging case of strongly connected systems.

The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO machines, generalizing similar existing results for flat counter machines. We also show that reachability is NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO machines. We construct a trace-flattable system of many counter machines communicating via rendez-vous that is bisimilar to a given flat FIFO machine, which allows to model-check the original flat FIFO machine. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO machines based on analysis of flat sub-machines.

Petri nets are a well-known model of concurrency and provide an ideal setting for the study of fundamental aspects in concurrent systems. Despite their simplicity, they still lack a satisfactory causally reversible semantics. We develop such semantics for Place/Transitions Petri nets (P/T nets) based on two observations. Firstly, a net that explicitly expresses causality and conflict among events, for example an occurrence net, can be straightforwardly reversed by adding a reverse transition for each of its forward transitions. Secondly, given a P/T net the standard unfolding construction associates with it an occurrence net that preserves all of its computation. Consequently, the reversible semantics of a P/T net can be obtained as the reversible semantics of its unfolding. We show that such reversible behaviour can be expressed as a finite net whose tokens are coloured by causal histories. Colours in our encoding resemble the causal memories that are typical in reversible process calculi.

This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability ("Rabin's Tree Theorem") is one of the most powerful known results concerning the decidability of logics. By a complete axiomatization we mean a complete deduction system with a polynomial-time recognizable set of axioms. By naive enumeration of formal derivations, this formally gives a proof of Rabin's Tree Theorem. The deduction system consists of the usual rules for second-order logic seen as two-sorted first-order logic, together with the natural adaptation In addition, it contains an axiom scheme expressing the (positional) determinacy of certain parity games. The main difficulty resides in the limited expressive power of the language of MSO. We actually devise an extension of MSO, called Functional (Monadic) Second-Order Logic (FSO), which allows us to uniformly manipulate (hereditarily) finite sets and corresponding labeled trees, and whose language allows for higher abstraction than that of MSO.

The BPMN 2.0 standard is a widely used semi-formal notation to model distributed information systems from different perspectives. The standard makes available a set of diagrams to represent such perspectives. Choreography diagrams represent global constraints concerning the interactions among system components without exposing their internal structure. Collaboration diagrams instead permit to depict the internal behaviour of a component, also referred as process, when integrated with others so to represent a possible implementation of the distributed system. This paper proposes a design methodology and a formal framework for checking conformance of choreographies against collaborations. In particular, the paper presents a direct formal operational semantics for both BPMN choreography and collaboration diagrams. Conformance aspects are proposed through two relations defined on top of the defined semantics. The approach benefits from the availability of a tool we have developed, named C4, that permits to experiment the theoretical framework in practical contexts. The objective here is to make the exploited formal methods transparent to system designers, thus fostering a wider adoption by practitioners.