Moreno Falaschi

TCS Journal 2021 Journal Article

A logical and graphical framework for reaction systems

• Linda Brodo
• Roberto Bruni
• Moreno Falaschi

Reaction Systems (RSs) are a successful computational framework inspired by biological systems. A RS pairs a set of entities with a set of reactions over them. Entities can be used to enable or inhibit each reaction, and are produced by reactions. Entities can also be provided by an external context sequence to simulate in silico biological experiments. In this paper we define an extension of RSs considering nondeterministic and recursive context operators, and give an original labelled transition system (LTS) for extended RSs in the structural operational semantics (SOS) style. Thanks to extended contexts, a single LTS can now account for several biological experiments. The rich information recorded in transition labels is useful to guarantee the compositionality of SOS inference rules as well as to define an assertion language to tailor behavioural and logical equivalences on some specific properties or entities. The SOS rules have been also exploited to design a flexible prototype implementation in logic programming that allows to inspect the LTS and to extract useful information when performing experiments on a RS. Our implementation provides a rapid prototyping tool for (extensions of) RSs, with a user friendly online interface to our interpreter. A parser allows to introduce the logical formulas and the contexts using the usual comfortable concrete syntax. The user can visualise and inspect the LTS for a RS and make some analysis of its underlying computation patterns, can check if the main RS satisfies a given property and if it is equivalent to a second adversarial RS. Finally, the SOS approach is suited to drive additional enhancements of RSs.

TCS Journal 2021 Journal Article

A process algebraic approach to reaction systems

• Linda Brodo
• Roberto Bruni
• Moreno Falaschi

In the area of Natural Computing, Reaction Systems (RSs) are a qualitative abstraction inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. RSs interact with a context, and pose challenges for modularity, compositionality, extendibility and behavioural equivalence. In this paper we define a modular encoding of RSs as processes in the chained Core Network Algebra (cCNA), which is a new variant of the link-calculus. The encoding represents the behaviour of each entity separately and preserves faithfully their features, and we prove its correctness and completeness. Our encoding provides a Labelled Transition System (LTS) semantics for RSs. Based on the LTS semantics, we adapt the classical notion of bisimulation to define a novel equivalence, called bio-similarity, for studying properties of RSs. In particular, we define a new assertion language based on regular expressions, which allows us to specify the properties of interest, and use it to extend Hennessy-Milner logic to our setting. We prove that our bio-similarity relation and the logical equivalence, that are defined parametrically on some assertion of interest, coincide. Finally, we claim that our encoding contributes to increase the expressiveness of RSs, by exploiting the interaction among different RSs.

LOPSTR Conference 2018 Conference Paper

An Assertion Language for Slicing Constraint Logic Languages

• Moreno Falaschi
• Carlos Olarte

Abstract Constraint Logic Programming (CLP) is a language scheme for combining two declarative paradigms: constraint solving and logic programming. Concurrent Constraint Programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints in a shared store. In a previous paper, we developed a framework for dynamic slicing of CCP where the user first identifies that a (partial) computation is wrong. Then, she marks (selects) some parts of the final state corresponding to the data (constraints) and processes that she wants to study more deeply. An automatic process of slicing begins, and the partial computation is “depurated” by removing irrelevant information. In this paper we give two major contributions. First, we extend the framework to CLP, thus generalizing the previous work. Second, we provide an assertion language suitable for both, CCP and CLP, which allows the user to specify some properties of the computations in her program. If a state in a computation does not satisfy an assertion then some “wrong” information is identified and an automatic slicing process can start. We thus make one step further towards automatizing the slicing process. We show that our framework can be integrated with the previous semi-automatic one, giving the user more choices and flexibility. We show by means of examples and experiments the usefulness of our approach.

LOPSTR Conference 2016 Conference Paper

Slicing Concurrent Constraint Programs

• Moreno Falaschi
• Maurizio Gabbrielli
• Carlos Olarte
• Catuscia Palamidessi

Abstract 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 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 timed variants of CCP. We also develop a prototypical implementation freely available for making experiments.

I&C Journal 2014 Journal Article

Functional and (Constraint) Logic Programming

• Santiago Escobar
• Moreno Falaschi

TCS Journal 2009 Journal Article

Foreword

• Moreno Falaschi
• Maurizio Gabbrielli
• Catuscia Palamidessi

TCS Journal 2004 Journal Article

Rules + strategies for transforming lazy functional logic programs

• Marı́a Alpuente
• Moreno Falaschi
• Ginés Moreno
• Germán Vidal

This work introduces a transformation methodology for functional logic programs based on needed narrowing, the optimal and complete operational principle for modern declarative languages which integrate the best features of functional and logic programming. We provide correctness results for the transformation system w. r. t. the set of computed values and answer substitutions and show that the prominent properties of needed narrowing—namely, the optimality w. r. t. the length of derivations and the number of computed solutions—carry over to the transformation process and the transformed programs. We illustrate the power of the system by taking on in our setting two well-known transformation strategies (composition and tupling). We also provide an implementation of the transformation system which, by means of some experimental results, highlights the potentiality of our approach.

JELIA Conference 2004 Conference Paper

Verdi: An Automated Tool for Web Sites Verification

• María Alpuente
• Demis Ballis
• Moreno Falaschi

Abstract Verdi is a system for the automated verification of Web sites which can be used to specify integrity conditions for a given Web site, and then automatically check whether these conditions are actually fulfilled. It provides a rule-based, formal specification language which allows us to define syntactic/semantic properties of the Web site as well as a verification facility which computes the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete/missing Web pages.

LOPSTR Conference 2002 Conference Paper

Abstract Diagnosis of Functional Programs

• María Alpuente
• Marco Comini
• Santiago Escobar 0001
• Moreno Falaschi
• Salvador Lucas

Abstract We present a generic scheme for the declarative debugging of functional programs modeled as term rewriting systems. We associate to our programs a semantics based on a (continuous) immediate consequence operator, \( T_\mathcal{R} \), which models the (values/normal forms) semantics of \( \mathcal{R} \). Then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of \( \mathcal{R} \) we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to either provide error symptoms in advance or answer questions concerning program correctness. We have made available a prototypical implementation in Haskell and have tested it on some non trivial examples.

TCS Journal 1997 Journal Article

Confluence in concurrent constraint programming

• Moreno Falaschi
• Maurizio Gabbrielli
• Kim Marriott
• Catuscia Palamidessi

Concurrent constraint programming (ccp), like most of the concurrent paradigms, has a mechanism of global choice which makes computations dependent on the scheduling of processes. This is one of the main reasons why the formal semantics of ccp is more complicated than the one of its deterministic and local-choice sublanguages. In this paper we study various subsets of ccp obtained by adding some restriction on the notion of choice, or by requiring confluency, i. e. independency from the scheduling strategy. We show that it is possible to define simple denotational semantics for these subsets, for various notions of observables. Finally, as an application of our results we develop a framework for the compositional analysis of full ccp. The basic idea is to approximate an arbitrary ccp program by a program in the restricted language, and then analyze the latter, by applying the standard techniques of abstract interpretation to its denotational semantics.

I&C Journal 1997 Journal Article

Constraint Logic Programming with Dynamic Scheduling: A Semantics Based on Closure Operators

• Moreno Falaschi
• Maurizio Gabbrielli
• Kim Marriott
• Catuscia Palamidessi

The first logic programming languages, such as Prolog, used a fixed left-to-right atom scheduling rule. Recent logic programming languages, however, provide more flexible scheduling in which there is a default computation rule such as left-to-right but in which some calls are dynamically “delayed” until their arguments are sufficiently instantiated to allow the call to run efficiently. Such languages include constraint logic programming languages, since most implementations of these languages delay constraints which are “too hard. ” From the semantic point of view, the fact that an atom must be delayed under certain conditions, causes the standard semantics of (constraint) logic programming to be no longer adequate to capture the meaning of a program. In our paper we attack this problem and we develop a denotational semantics for constraint logic programming with dynamic scheduling. The key idea is that the denotation of an atom or goal is a set of closure operators, where different closure operators correspond to different sequences of rule choices.

TCS Journal 1996 Journal Article

A compositional semantic basis for the analysis of equational Horn programs

• María Alpuente
• Moreno Falaschi
• Germán Vidal

We introduce a compositional characterization of the operational semantics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we show a compositional analysis to detect the unsatisfiability of an equation set with respect to a given equational theory. We also show that our method allows us to perform computations and analysis incrementally in a Constraint Equational setting and that the test of satisfiability in this setting can be done in parallel.

TCS Journal 1995 Journal Article

Incremental constraint satisfaction for equational logic programming

• María Alpuente
• Moreno Falaschi
• Giorgio Levi

In this paper we are concerned with an instance of the Constraint Logic Programming (CLP) scheme specialized in solving equations with respect to a Horn equational theory E. The intended structure H E is given by the finest partition induced by E on the Herbrand universe H over a finite one sorted alphabet. This work deals with the description of an incremental constraint solver as the kernel of an operational semantics for the language CLP( H E ). The primary issues are: how to verify the solvability of constraints in the structure ( H E ) by using some sound and complete semantic unification procedure such as narrowing, how to simplify constraints in a computation sequence, how to achieve incrementality in the computation process and how to profit from finitely failed derivations as a heuristic for optimizing the algorithms.

TCS Journal 1990 Journal Article

Finite failures and partial computations in concurrent logic languages

• Moreno Falaschi
• Giorgio Levi

This paper investigates some semantic properties of concurrent logic languages. Concurrent logic languages with a commit operator differ from pure logic languages in the finite failure set. Since the new finite failure set depends on the computation rule, we define an operational semantics based on a parallel computation rule and a fair search rule. Failures with a parallel computation rule are shown to be strongly related to partial computed answer substitutions. The set of partial computed answer substitutions and the set of finite failures are defined as the least fixpoint of a transformation on pairs of interpretations.