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

Knowledge Graph Embeddings (KGE) have become a quite popular class of models specifically devised to deal with ontologies and graph structure data, as they can implicitly encode statistical dependencies between entities and relations in a latent space. KGE techniques are particularly effective for the biomedical domain, where it is quite common to deal with large knowledge graphs underlying complex interactions between biological and chemical objects. Recently in the literature, the PharmKG dataset has been proposed as one of the most challenging knowledge graph biomedical benchmark, with hundreds of thousands of relational facts between genes, diseases and chemicals. Despite KGEs can scale to very large relational domains, they generally fail at representing more complex relational dependencies between facts, like logic rules, which may be fundamental in complex experimental settings. In this paper, we exploit logic rules to enhance the embedding representations of KGEs on the PharmKG dataset. To this end, we adopt Relational Reasoning Network (R2N), a recently proposed neural-symbolic approach showing promising results on knowledge graph completion tasks. An R2N uses the available logic rules to build a neural architecture that reasons over KGE latent representations. In the experiments, we show that our approach is able to significantly improve the current state-of-the-art on the PharmKG dataset. Finally, we provide an ablation study to experimentally compare the effect of alternative sets of rules according to different selection criteria and varying the number of considered rules.

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.

Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language ntcc, linear CCP (an extension of CCPbased on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments.

No abstract available.

Abstract Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e., systems that continuously interact with the environment. The universaltccformalism (utcc) is an extension oftccwith the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics fortcc, and extend it to a “collecting” semantics forutccbased on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses oftccandutccprograms by abstract interpretation techniques. The concrete and abstract semantics that we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis fortccprograms. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show thattccprograms are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging.

Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we present a fold/unfold-based transformation framework for rewriting logic theories which is based on narrowing. For the best of our knowledge, this is the first fold/unfold transformation framework which allows one to deal with functions, rules, equations, sorts, and algebraic laws (such as commutativity and associativity). We provide correctness results for the transformation system w.r.t. the semantics of ground reducts. Moreover, we show how our transformation technique can be naturally applied to implement a Code Carrying Theory (CCT) system. CCT is an approach for securing delivery of code from a producer to a consumer where only a certificate (usually in the form of assertions and proofs) is transmitted from the producer to the consumer who can check its validity and then extract executable code from it. Within our framework, the certificate consists of a sequence of transformation steps which can be applied to a given consumer specification in order to automatically synthesize safe code in agreement with the original requirements. We also provide an implementation of the program transformation framework in the high-performance, rewriting logic language Maude which, by means of an experimental evaluation of the system, highlights the potentiality of our approach.

Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e. systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and we extend it to a "collecting" semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize the first general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric w.r.t. the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming, e.g., to perform a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we make also use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We have developed a prototypical implementation of our methodology and we have implemented the abstract domain for security to perform automatically the secrecy analysis.

In this paper, we present an extension of PHIL, a declarative language for filtering information from XML data. The proposed approach allows us to extract relevant data as well as to exclude useless and misleading contents from an XML document. Essentially, it combines ontology reasoning with an approximate pattern-matching engine which searches for patterns in a flexible way (i.e. modulo renaming, insertion, and deletion of XML items) and ranks the results w.r.t. their cost. The filtering process is guided by the syntax as well as the semantics of the XML documents, since it relies on both the document structure and the onto- logical information to which the document is related. Such information is retrieved by querying (possibly remote) ontology reasoners. Our methodology has been implemented in the XPHIL system, which is written in Haskell. By using the XML benchmarking tool xmlgen, we have developed some scalable experiments which demonstrate the usefulness of our approach.

In recent years much research and implementation effort has been devoted both to multiparadigm languages and constraint programming languages. Following up on a series of 11 workshops (WFLP) on multiparadigm languages and constraint programming, and as a result of an open call for submissions, the journal on Theory and Practice of Logic Programming is now publishing the results of the selection of the papers submitted to this special issue.

The development and maintenance of Web sites are difficult tasks. To maintain the consistency of ever-larger, complex Web sites, Web administrators need effective mechanisms that assist them in fixing every possible inconsistency. In this paper, we present a novel methodology for semi-automatically repairing faulty Web sites which can be integrated on top of an existing rewriting-based verification technique developed in a previous work. Starting from a categorization of the kinds of errors that can be found during the Web verification activities, we formulate a stepwise transformation procedure that achieves correctness and completeness of the Web site w.r.t. its formal specification while respecting the structure of the document (e.g. the schema of an XML document). Finally, we shortly describe a prototype implementation of the repairing tool which we used for an experimental evaluation of our method

The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.

Needed narrowing is a complete and optimal operational principle for modern declarative languages which integrate the best features of lazy functional and logic programming. We investigate the formal relation between needed narrowing and another (not so lazy) narrowing strategy which is the basis for popular implementations of lazy functional logic languages. We demonstrate that needed narrowing and lazy narrowing are computationally equivalent over the class of uniform programs. We also introduce a complete refinement of lazy narrowing, called uniform lazy narrowing, which is still equivalent to needed narrowing over the aforementioned class. Since actual implementations of functional logic languages are based on the transformation of the original program into a uniform one—which is then executed using a lazy narrowing strategy—our results can be thought of as a formal basis for the correctness of these implementations.

Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution principle of logic languages. In this article, we present a partial evaluation scheme for functional logic languages based on an automatic unfolding algorithm which builds narrowing trees. The method is formalized within the theoretical framework established by Lloyd and Shepherdson for the partial deduction of logic programs, which we have generalized for dealing with functional computations. A generic specialization algorithm is proposed which does not depend on the eager or lazy nature of the narrower being used. To the best of our knowledge, this is the first generic algorithm for the specialization of functional logic programs. We also discuss the relation to work on partial evaluation in functional programming, term-rewriting systems, and logic programming. Finally, we present some experimental results with an implementation of the algorithm which show in practice that the narrowing-driven partial evaluator effectively combines the propagation of partial data structures (by means of logical variables and unification) with better opportunities for optimization (thanks to the functional dimension).

Partial evaluation is a method for program specialization based on fold/unfold transformations [8, 25]. Partial evaluation of pure functional programs uses mainly static values of given data to specialize the program [15, 44]. In logic programming, the so-called static/dynamic distinction is hardly present, whereas considerations of determinacy and choice points are far more important for control [12]. We discuss these issues in the context of a (lazy) functional logic language. We formalize a two-phase specialization method for a non-strict, first order, integrated language which makes use of lazy narrowing to specialize the program w.r. t. a goal. The basic algorithm (first phase) is formalized as an instance of the framework for the partial evaluation of functional logic programs of [2, 3], using lazy narrowing. However, the results inherited by [2, 3] mainly regard the termination of the PE method, while the (strong) soundness and completeness results must be restated for the lazy strategy. A post-processing renaming scheme (second phase) is necessary which we describe and illustrate on the well-known matching example. This phase is essential also for other non-lazy narrowing strategies, like innermost narrowing, and our method can be easily extended to these strategies. We show that our method preserves the lazy narrowing semantics and that the inclusion of simplification steps in narrowing derivations can improve control during specialization.

Concurrent logic languages specify reactive systems which consist of collections of communicating processes. The presence of unintended suspended computations is a common programming error which is difficult to detect using standard debugging and testing techniques. We develop a number of analyses, based on abstract interpretation, which succeed if a program is definitely suspension free. If an analysis fails, the program may, or may not, be suspension free. Examples demonstrate that the analyses are practically useful. They are conceptually simple and easy to justify because they are based directly on the transition system semantics of concurrent logic programs. A naive analysis must consider all scheduling policies . However, it is proven that for our analyses it suffices to consider only one scheduling policy, allowing for efficient implementation.

A framework for the analysis of concurrent constraint programming (CCP) is proposed. The approach is based on simple denotational semantics that approximate the usual semantics in the sense that they give a superset of the input-output relation of a CCP program. Analyses based on these semantics can be easily and efficiently implemented using standard techniques from the analysis of logic programs.>