O'Hearn's Incorrectness Logic (IL) has sparked renewed interest in static analyses that aim to detect program errors rather than prove their absence, thereby avoiding false alarms—a critical factor for practical adoption in industrial settings. As new incorrectness logics emerge to capture diverse error-related properties, a key question arises: can combining correctness and incorrectness techniques enhance precision, expressiveness, automation, or scalability? Notable frameworks, such as outcome logic, UNTer, local completeness logic, and exact separation logic, unify multiple analyses within a single proof system. In this work, we adopt a complementary strategy. Rather than designing a unified logic, we combine IL, which identifies reachable error states, with Sufficient Incorrectness Logic (SIL), which finds input states potentially leading to those errors. As a result, we get a more informative and effective analysis than either logic in isolation. Rather than sequencing them, our key innovation is reusing heuristic choices from the first analysis to steer the second. In fact, both IL and SIL rely on under-approximation and thus their automation legitimizes heuristics that avoid exhaustive path enumeration (e.g., selective disjunct pruning, loop unrolling). Concretely, we instrument the proof rules of the second logic with derivations from the first to inductively guide rule selection and application. To our knowledge, this is the first rule format enabling such inter-analysis instrumentation. This combined analysis aids debugging and testing by revealing both reachable errors and their causes, and opens new avenues for embedding incorrectness insights into scalable, expressive, automated code contracts.

Abstract Reaction Systems (RSs) are a qualitative model inspired by biochemical processes, where the dynamics of complex systems is modelled by a collection of local reactions. Each reaction comprises a set of reactants that triggers a set of products unless hindered by the presence of some inhibitors. The use of inhibitors introduces non-monotonic behaviours that are difficult to analyze. This work focuses on the explainability of local phenomena, like the production of certain products or the reachability of certain attractors, by separating the causes responsible for reaching them from the irrelevant elements of a possibly much larger, global statespace. The main novelty of our approach is the ability to derive sufficient conditions that combine positive dependencies (e.g., requesting the presence of some entities at a certain stage, as already done in the literature) with negative ones (e.g., requesting the absence of some entities). This is achieved by combining and extending previous “static” constructions, like the transformation to Positive RSs and the minimization of RSs with “dynamic” techniques, like the process algebraic evolution of RSs, the slicing of computation and the on-the-fly generation of negative dependencies. We compare many different combinations of the above approaches, discussing their respective benefits and trade-offs in order to identify the most convenient analysis. We demonstrate our methodology on a case study involving T cell protein interactions, showing how it can reveal critical stimulus combinations and pinpoint potential drug targets by explaining phenotype emergence. Our analysis offers new insights and greater explanatory power than existing approaches.

Abstract We explore the capabilities of , a state-of-the-art toolset based on graph transformation systems, to perform different kinds of analyses of Reaction Systems, ranging from reachability and causal analysis to model checking. Our results are encouraging, as in the presence of large state spaces improves the time required for both reachability and causal analyses by an order of magnitude, compared to other available tools. From the point of view of , the implementation of Reaction Systems provided some interesting insights on the most convenient way to model certain computational requirements through negative and nested application conditions.

Sound over-approximation methods are effective for proving the absence of errors, but inevitably produce false alarms that can hamper programmers. In contrast, under-approximation methods focus on bug detection and are free from false alarms. In this work, we present two novel proof systems designed to locate the source of errors via backward under-approximation, namely Sufficient Incorrectness Logic (SIL) and its specialization for handling memory errors, called Separation SIL. The SIL proof system is minimal, sound and complete for Lisbon triples, enabling a detailed comparison of triple-based program logics across various dimensions, including negation, approximation, execution order, and analysis objectives. More importantly, SIL lays the foundation for our main technical contribution, by distilling the inference rules of Separation SIL, a sound and (relatively) complete proof system for automated backward reasoning in programs involving pointers and dynamic memory allocation. The completeness result for Separation SIL relies on a careful crafting of both the assertion language and the rules for atomic commands.

Local Completeness Logic (LCL) is a proof system for program analysis rooted in abstract interpretation. The program semantics is under-approximated by any provable postcondition, like incorrectness logic does, but it is also over-approximated by a (locally) complete abstraction of such a postcondition, like Hoare logic does. Therefore, any derivable triple will either prove the program to be correct or unveil true bugs. While the completeness of a program's function with respect to an abstract domain is inherently extensional , LCL's rules demand the preservation of local completeness throughout the abstract interpreter's computations. This characteristic renders LCL analysis intensional , meaning it depends on the way the program is written. Consequently, LCL proof system may not derive all the valid triples. This paper addresses this discrepancy by: 1) designing new rules that allow one to perform part of the intensional analysis in different (complete) abstract domains whenever necessary; and 2) to compare their expressiveness. Notably, some of these new rules enable the derivation of all extensionally valid triples, thereby decoupling the set of provable properties from the way the program is written.

Abstract Reaction systems (RSs) are a computational framework inspired by biochemical mechanisms. A RS defines a finite set of reactions over a finite set of entities. Typically each reaction has a local scope, because it is concerned with a small set of entities, but complex models can involve a large number of reactions and entities, and their computation can manifest unforeseen emerging behaviours. When a deviation is detected, like the unexpected production of some entities, it is often difficult to establish its causes, e.g., which entities were directly responsible or if some reaction was misconceived. Slicing is a well-known technique for debugging, which can point out the program lines containing the faulty code. In this paper, we define the first dynamic slicer for RSs and show that it can help to detect the causes of erroneous behaviour and highlight the involved reactions for a closer inspection. To fully automate the debugging process, we propose to distil monitors for starting the slicing whenever a violation from a safety specification is detected. We have integrated our slicer in BioResolve, written in Prolog which provides many useful features for the formal analysis of RSs. We define the slicing algorithm for basic RSs and then enhance it for dealing with quantitative extensions of RSs, where timed processes and linear processes can be represented. Our framework is shown at work on suitable biologically inspired RS models.

Abstract This paper forges a strong connection between two well known computational frameworks for representing biological systems, in order to facilitate the seamless transfer of techniques between them. Boolean networks are a well established formalism employed from biologists. They have been studied under different (synchronous and asynchronous) update semantics, enabling the observation and characterisation of distinct facets of system behaviour. Recently, a new semantics for Boolean networks has been proposed, called most permissive semantics, that enables a more faithful representation of biological phenomena. Reaction systems offer a streamlined formalism inspired by biochemical reactions in living cells. Reaction systems support a full range of analysis techniques that can help for gaining deeper insights into the underlying biological phenomena. Our goal is to leverage the available toolkit for predicting and comprehending the behaviour of reaction systems within the realm of Boolean networks. In this paper, we first extend the behaviour of reaction systems to several asynchronous semantics, including the most permissive one, and then we demonstrate that Boolean networks and reaction systems exhibit isomorphic behaviours under the synchronous, general/fully asynchronous and most permissive semantics.

Abstract Cause/effect analysis of complex systems is instrumental in better understanding many natural phenomena. Moreover, formal analysis requires the availability of suitable abstract computational models that somehow preserve the features of interest. Our contribution focuses on the analysis of Reaction Systems (RSs), a qualitative computational formalism inspired by biochemical reactions in living cells. The primary challenge lies in dealing with inhibition mechanisms. On the one hand, inhibitors enhance the expressiveness of the computational abstraction; on the other hand, they can introduce nonmonotonic behaviors that can be computationally hard to deal with in the analysis. We propose an encoding of RSs into an equivalent formulation without inhibitors (called Positive RSs, PRSs for short) that is easier to handle, because PRSs exhibit monotonic behaviors. The effectiveness of our transformation is witnessed by its impact on two different techniques for cause/effect analysis. The first, called slicing, allows detecting the causes of some unforeseen phenomenon by reasoning backward along a given computation. Here, PRSs can be exploited to improve the quality of the analysis. The second technique, predictor analysis, is addressed by introducing a novel tool called MuMa, which is based on must/maybe sets, whence the tool name, an original abstraction for approximating ancestor formulas. MuMa exploits PRSs to improve the performance of the analysis.

The main goal of most static analyses is to prove the absence of bugs : if the analysis reports no alarms, then the program will not exhibit any unwanted behaviours. For this reason, they are designed to over-approximate program behaviours and, consequently, they can report some false alarms. O’Hearn’s recent work on incorrectness has renewed the interest in the use of under-approximations for bug finding , because they only report true alarms. In principle, Abstract Interpretation techniques can handle under-approximations as well as over-approximations, but, in practice, few attempts were developed for the former, notwithstanding the much wider literature on the latter. In this article, we investigate the possibility of exploiting under-approximation abstract domains for bug-finding analyses. First we restrict to consider concrete powerset domains and highlight some intuitive asymmetries between over- and under-approximations. Then, we prove that the effectiveness of abstract domains defined by under-approximation Galois connection is limited because the analysis is likely to return trivial results whenever common transfer functions are encoded in the program. To this aim, we introduce the original concepts of non-emptying functions and highly surjective function family , and we prove the nonexistence of abstract domains able to under-approximate such functions in a non-trivial way. We show many examples of finite and infinite numerical domains, as well as other generic domains. In all such cases, we prove the impossibility of performing non-trivial analyses via under-approximation Galois connections.

Abstract We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.

Abstract Abstract interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness Logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple $$\vdash _{A}[P]~\textsf{c}~[Q]$$ ⊢ A [ P ] c [ Q ] in the logic implies completeness of an intensional abstraction of program $$\textsf{c}$$ c on input P and is such that Q can be used to decide (in)correctness. However, completeness itself is an extensional property of the function computed by the program, while the above intensional analysis depends on the way the program is written and therefore not all valid triples can be derived in the proof system. Our main contribution is the study of new inference rules which allow one to perform part of the intensional analysis in a more precise abstract domain, and then to transfer the result back to the coarser domain. With these new rules, all (extensionally) valid triples can be derived in the proof system, thus untying the set of provable properties from the way the program is written.

Abstract interpretation is a well-known and extensively used method to extract over-approximate program invariants by a sound program analysis algorithm. Soundness means that no program errors are lost and it is, in principle, guaranteed by construction. Completeness means that the abstract interpreter reports no false alarms for all possible inputs, but this is extremely rare because it needs a very precise analysis. We introduce a weaker notion of completeness, called local completeness , which requires that no false alarms are produced only relatively to some fixed program inputs. Based on this idea, we introduce a program logic, called Local Completeness Logic for an abstract domain A , for proving both the correctness and incorrectness of program specifications. Our proof system, which is parameterized by an abstract domain A , combines over- and under-approximating reasoning. In a provable triple ⊦ A [ p ] 𝖼 [ q ], 𝖼 is a program, q is an under-approximation of the strongest post-condition of 𝖼 on input p such that their abstractions in A coincide. This means that q is never too coarse, namely, under some mild assumptions, the abstract interpretation of 𝖼 does not yield false alarms for the input p iff q has no alarm . Therefore, proving ⊦ A [ p ] 𝖼 [ q ] not only ensures that all the alarms raised in q are true ones, but also that if q does not raise alarms, then 𝖼 is correct. We also prove that if A is the straightforward abstraction making all program properties equivalent, then our program logic coincides with O’Hearn’s incorrectness logic, while for any other abstraction, contrary to the case of incorrectness logic, our logic can also establish program correctness.

Abstract Reaction systems (RSs) are a successful natural computing framework inspired by chemical reaction networks. A RS consists of a set of entities and a set of reactions. Entities can enable or inhibit each reaction and are produced by reactions or provided by the environment. In this paper, we define two quantitative variants of RSs: the first one is along the time dimension, to specify delays for making available reactions products and durations to protract their permanency, while the second deals with the possibility to specify different concentration levels of a substance in order to enable or inhibit a reaction. Technically, both extensions are obtained by modifying in a modular way the Structural Operational Semantics (SOS) for RSs that was already defined in the literature. Our approach maintains several advantages of the original semantics definition that were: (1) providing a formal specification of the RS dynamics that enables the reuse of many formal analysis techniques and favours the implementation of tools, and (2) making the RS framework extensible, by adding or changing some of the SOS rules in a compositional way. We provide a prototype logic programming implementation and apply our tool to three different case studies: the tumour growth, the Th cell differentiation in the immune system and neural communication.

Abstract Static analyses are mostly designed to show the absence of bugs: if the analysis reports no alarms then the program won’t exhibit any unwanted behaviours. To this aim they manipulate over-approximations of program semantics and, inevitably, they often report some false alarms. Recently, O’Hearn proposed Incorrectness Logic, that is based on under-approximations, as a formal method to find bugs that only reports true alarms. In this paper we aim to answer one important question raised by O’Hearn, namely which role can Abstract Interpretation play for the development of under-approximate tools for bug catching. In principle, Abstract Interpretation based static analyses can be defined for computing over-approximations as well as under-approximations, but in practice, most techniques exploited the former while few attempts developed the latter. To show why it is difficult to design effective under-approximation abstract domains, we first propose the new definitions of non emptying functions and highly surjective function family and then we formally prove the limits of under-approximation analysis by showing the non existence of abstract domains able to approximate such functions in a non trivial way. Our results outline the limits of under-approximation Abstract Interpretation and clarify, for the first time, why over- and under- approximation analyzers exhibited such a different development.

Abstract interpretation is a sound-by-construction method for program verification: any erroneous program will raise some alarm. However, the verification of correct programs may yield false-alarms, namely it may be incomplete. Ideally, one would like to perform the analysis on the most abstract domain that is precise enough to avoid false-alarms. We show how to exploit a weaker notion of completeness, called local completeness, to optimally refine abstract domains and thus enhance the precision of program verification. Our main result establishes necessary and sufficient conditions for the existence of an optimal, locally complete refinement, called pointed shell. On top of this, we define two repair strategies to remove all false-alarms along a given abstract computation: the first proceeds forward, along with the concrete computation, while the second moves backward within the abstract computation. Our results pave the way for a novel modus operandi for automating program verification that we call Abstract Interpretation Repair (AIR): instead of choosing beforehand the right abstract domain, we can start in any abstract domain and progressively repair its local incompleteness as needed. In this regard, AIR is for abstract interpretation what CEGAR is for abstract model checking.

We introduce the notion of local completeness in abstract interpretation and define a logic for proving both the correctness and incorrectness of some program specification. Abstract interpretation is extensively used to design sound-by-construction program analyses that over-approximate program behaviours. Completeness of an abstract interpretation A for all possible programs and inputs would be an ideal situation for verifying correctness specifications, because the analysis can be done compositionally and no false alert will arise. Our first result shows that the class of programs whose abstract analysis on A is complete for all inputs has a severely limited expressiveness. A novel notion of local completeness weakens the above requirements by considering only some specific, rather than all, program inputs and thus finds wider applicability. In fact, our main contribution is the design of a proof system, parameterized by an abstraction A, that, for the first time, combines over- and under-approximations of program behaviours. Thanks to local completeness, in a provable triple ⊢A [P ] c [Q], the assertion Q is an under-approximation of the strongest post-condition post[c](P ) such that the abstractions in A of Q and post[c](P ) coincide. This means that Q is never too coarse, namely, under mild assumptions, the abstract interpretation of c does not yield false alerts for the input P iff Q has no alert. Thus, ⊢ A [P ] c [Q] not only ensures that all the alerts raised in Q are true ones, but also that if Q does not raise alerts then c is correct.

We present the link-calculus, an extension of π-calculus, that models interactions that are multiparty, i.e. that may involve more than two processes, mutually exchanging data. Communications are seen as chains of suitably combined links (which record the source and the target ends of each hop of interactions), each contributed by one party. Values are exchanged by means of message tuples, still provided by each party. We develop semantic theories and proof techniques for link-calculus and apply them in reasoning about complex distributing computing scenarios, where more than two participants need to synchronise in order to perform a task. In particular, we introduce the notion of linked bisimilarity in analogy with the early bisimilarity of the π-calculus. Differently from the π-calculus case, we can show that it is a congruence with respect to all the link-calculus operators and that is also closed under name substitution.

In this paper we generalise the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations . The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.

Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general solution based on a recursive, static decomposition of (occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-cell exposes a set of alternatives, called transactions. Our solution transforms a given Petri net into another net whose transitions are the transactions of the s-cells and whose places are those of the original net, with some auxiliary structure for bookkeeping. The resulting net is confusion-free, and thus conflicting alternatives can be equipped with probabilistic choices, while nonintersecting alternatives are purely concurrent and their probability distributions are independent. The validity of the construction is witnessed by a tight correspondence with the recursively stopped configurations of Abbes and Benveniste. Some advantages of our approach are that: i) s-cells are defined statically and locally in a compositional way; ii) our resulting nets faithfully account for concurrency.

Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general solution based on a recursive, static decomposition of (occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-cell exposes a set of alternatives, called transactions. Our solution transforms a given Petri net into another net whose transitions are the transactions of the s-cells and whose places are those of the original net, with some auxiliary structure for bookkeeping. The resulting net is confusion-free, and thus conflicting alternatives can be equipped with probabilistic choices, while nonintersecting alternatives are purely concurrent and their probability distributions are independent. The validity of the construction is witnessed by a tight correspondence with the recursively stopped configurations of Abbes and Benveniste. Some advantages of our approach are that: i) s-cells are defined statically and locally in a compositional way; ii) our resulting nets faithfully account for concurrency.

Abstract Code protection technologies require anti reverse engineering transformations to obfuscate programs in such a way that tools and methods for program analysis become ineffective. We introduce the concept of model deformation inducing an effective code obfuscation against attacks performed by abstract model checking. This means complicating the model in such a way a high number of spurious traces are generated in any formal verification of the property to disclose about the system under attack.We transform the program model in order to make the removal of spurious counterexamples by abstraction refinement maximally inefficient. Because our approach is intended to defeat the fundamental abstraction refinement strategy, we are independent from the specific attack carried out by abstract model checking. A measure of the quality of the obfuscation obtained by model deformation is given together with a corresponding best obfuscation strategy for abstract model checking based on partition refinement.

Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a uniquely determined set of causes. Prime event structures, in turn, can be identified with their domain of configurations. At a categorical level, this is nicely formalised by Winskel as a chain of coreflections. Contrary to prime event structures, general event structures allow for the presence of disjunctive causes, i.e., events can be enabled by distinct minimal sets of events. In this paper, we extend the connection between Petri nets and event structures in order to include disjunctive causes. In particular, we show that, at the level of nets, disjunctive causes are well accounted for by persistent places. These are places where tokens, once generated, can be used several times without being consumed and where multiple tokens are interpreted collectively, i.e., their histories are inessential. Generalising the work on ordinary nets, Petri nets with persistence are related to a new subclass of general event structures, called locally connected, by means of a chain of coreflections relying on an unfolding construction.

Service-oriented computing is calling for novel computational models and languages with well-disciplined primitives for client–server interaction, structured orchestration and unexpected events handling. We present CaSPiS, a process calculus where the conceptual abstractions of sessioning and pipelining play a central role for modelling service-oriented systems. CaSPiS sessions are two-sided, uniquely named and can be nested. CaSPiS pipelines permit orchestrating the flow of data produced by different sessions. The calculus is also equipped with operators for handling (unexpected) termination of the partner's side of a session. Several examples are presented to provide evidence of the flexibility of the chosen set of primitives. One key contribution is a fully abstract encoding of Misra et al.'s orchestration language Orc. Another main result shows that in CaSPiS it is possible to program a ‘graceful termination’ of nested sessions, which guarantees that no session is forced to hang forever after the loss of its partner.

This paper proposes a formal approach to the design and programming of long running transactions (LRTs). We exploit techniques from process calculi to define cJoin, which is an extension of the Join calculus with few well-disciplined primitives for LRT. Transactions in cJoin are intended to describe the transactional interaction of several partners, under the assumption that any partner executing a transaction may communicate only with other transactional partners. In such case, the transactions run by any party are bound to achieve the same outcome (i.e., all succeed or all fail). Hence, a distinguishing feature of cJoin, called dynamic joinability, is that ongoing transactions can be merged to complete their tasks and when this happens either all succeed or all abort. Additionally, cJoin is based on compensations i.e., partial executions of transactions are recovered by executing user-defined programs instead of providing automatic rollback. The expressiveness and generality of cJoin is demonstrated by many examples addressing common programming patterns. The mathematical foundation is accompanied by a prototype language implementation, which is an extension of the JoCaml compiler.

Compositional graph models for global computing systems must account for two relevant dimensions, namely structural containment and communication linking. In Milner's bigraphs the two dimensions are made explicit and represented as two loosely coupled structures: the place graph and the link graph. Here, bigraphs are compared with an earlier model, gs-graphs, originally conceived for modelling the syntactical structure of agents with α-convertible declarations. We show that gs-graphs are quite convenient also for the new purpose, since the two above mentioned dimensions can be recovered by considering only a specific class of hyper-signatures. With respect to bigraphs, gs-graphs can be proved essentially equivalent, with minor differences at the interface level. We argue that gs-graphs offer a simpler and more standard algebraic structure, based on monoidal categories, for representing both states and transitions. Moreover, they can be equipped with a simple type system to check the well-formedness of legal gs-graphs that are shown to characterise binding bigraphs. Another advantage concerns a textual form in terms of sets of assignments, which can make implementation easier in rewriting frameworks like Maude.

A key aspect when aggregating business processes and web services is to assure transactional properties of process ex-ecutions. Since transactions in this context may require long periods of time to complete, traditional mechanisms for guaranteeing atomicity are not always appropriate. Gen-erally the concept of long running transactions relies on a weaker notion of atomicity based on compensations. For this reason, programming languages for service composition cannot leave out two key aspects: compensations, i.e. ad hoc activities that can undo the effects of a process that fails to complete, and transactional boundaries to delimit the scope of a transactional flow. This paper presents a hierarchy of transactional calculi with increasing expressiveness. We start from a very small language in which activities can only be composed sequentially. Then, we progressively introduce parallel composition, nesting, programmable compensations and exception handling. A running example illustrates the main features of each calculus in the hierarchy.

Nowadays concepts, languages and models for coordination cannot leave aside the needs of the increasing number of commercial applications based on global computing over the (inter)net. For example, platforms like Microsoft .NET and Sun Microsystems Java come equipped with packages for supporting ad hoc transactional features, which are essential for most business applications. We show how to extend the coordination language par excellence (viz. Linda) with basic primitives for transactions, while retaining a formal model for its concurrent computations. This is achieved by exploiting a variation of Petri nets, called zero-safe nets, where transactions can be suitably modelled by distinguishing between stable places (ordinary ones) and zero places (where tokens can only be temporarily allocated, defining hidden states). The relevance of the transaction mechanism is illustrated in terms of expressive power. Finally, it is shown that stable places and transactions viewed as atomic steps define an abstract semantics that is apt for a fully algebraic treatment, as demonstrated via categorical adjunctions between suitable categories of nets.

Tile systems offer a general paradigm for modular descriptions of concurrent systems, based on a set of rewriting rules with side-effects. Monoidal double categories are a natural semantic framework for tile systems, because the mathematical structures describing system states and synchronizing actions (called configurations and observations, respectively, in our terminology) are monoidal categories having the same objects (the interfaces of the system). In particular, configurations and observations based on net-process-like and term structures are usually described in terms of symmetric monoidal and cartesian categories, where the auxiliary structures for the rearrangement of interfaces correspond to suitable natural transformations. In this paper we discuss the lifting of these auxiliary structures to double categories. We notice that the internal construction of double categories produces a pathological asymmetric notion of natural transformation, which is fully exploited in one dimension only (for example, for configurations or for observations, but not for both). Following Ehresmann (1963), we overcome this biased definition, introducing the notion of generalized natural transformation between four double functors (rather than two). As a consequence, the concepts of symmetric monoidal and cartesian (with consistently chosen products) double categories arise in a natural way from the corresponding ordinary versions, giving a very good relationship between the auxiliary structures of configurations and observations. Moreover, the Kelly–Mac Lane coherence axioms can be lifted to our setting without effort, thanks to the characterization of two suitable diagonal categories that are always present in a double category. Then, symmetric monoidal and cartesian double categories are shown to offer an adequate semantic setting for process and term tile systems.

We apply to logic programming some recently emerging ideas from the field of reductionbased communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms that rule the operational machinery of such a programming paradigm. The semantic framework we have chosen for presenting our results is tile logic, which has the advantage of allowing a uniform treatment of goals and observations and of applying abstract categorical tools for proving the results. As main contributions, we mention the finitary presentation of abstract unification, and a concurrent and coordinated abstract semantics consistent with the most common semantics of logic programming. Moreover, the compositionality of the tile semantics is guaranteed by standard results, as it reduces to check that the tile systems associated to logic programs enjoy the tile decomposition property. An extension of the approach for handling constraint systems is also discussed.

We introduce the notion of cartesian closed double category to provide mobile calculi for communicating systems with specific semantic models: One dimension is dedicated to compose systems and the other to compose their computations and their observations. Also, inspired by the connection between simply typed /spl lambda/-calculus and cartesian closed categories, we define a new typed framework, called double /spl lambda/-notation, which is able to express the abstraction/application and pairing/projection operations in all dimensions. In this development, we take the categorical presentation as a guidance in the interpretation of the formalism. A case study of the /spl pi/-calculus, where the double /spl lambda/-notation straightforwardly handles name passing and creation, concludes the presentation.