-
Chapter and Conference Paper
Simulation of Kohn’s Molecular Interaction Maps through Translation into Stochastic CLS+
Kohn’s Molecular Interaction Maps (MIMs) are a graphical notation for describing bioregulatory networks at the molecular level. Even if the meaning of Kohn’s diagrams can be often easily understood, in many ca...
-
Chapter and Conference Paper
Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates
We present an abstraction of the probabilistic semantics of Multiset Rewriting to formally express systems of reactions with uncertain kinetic rates. This allows biological systems modelling when the exact rat...
-
Article
Bisimulations in calculi modelling membranes
Bisimulations are well-established behavioural equivalences that are widely used to study properties of computer science systems. Bisimulations assume the behaviour of systems to be described as labelled trans...
-
Chapter and Conference Paper
Stochastic Calculus of Loo** Sequences for the Modelling and Simulation of Cellular Pathways
The paper presents the Stochastic Calculus of Loo** Sequences (SCLS) suitable to describe microbiological systems, such as cellular pathways, and their evolution. Systems are represented by terms. The terms ...
-
Chapter and Conference Paper
The Calculus of Loo** Sequences
We describe the Calculus of Loo** Sequences (CLS) which is suitable for modeling microbiological systems and their evolution. We present two extensions, CLS with links (LCLS) and Stochastic CLS. LCLS simplif...
-
Chapter and Conference Paper
Extending the Calculus of Loo** Sequences to Model Protein Interaction at the Domain Level
In previous papers we introduced a formalism, called Calculus of Loo** Sequences (CLS), for describing biological systems and their evolution. CLS is based on term rewriting. Terms can be constructed by comp...
-
Chapter and Conference Paper
The Calculus of Loo** Sequences for Modeling Biological Membranes
We survey the formalism Calculus of Loo** Sequences (CLS) and a number of its variants from the point of view of their use for describing biological membranes. The CLS formalism is based on term rewriting an...
-
Chapter and Conference Paper
Bisimulation Congruences in the Calculus of Loo** Sequences
The Calculus of Loo** Sequences (CLS) is a calculus suitable to describe biological systems and their evolution. CLS terms are constructed by starting from basic constituents and composing them by means of o...
-
Article
Reduced Models for Efficient CCS Verification
Verification of a concurrent system can be accomplished by model checking the properties on a structure representing the system; this structure is, in general, a transition system which contains a prohibitive ...
-
Article
Timed automata with urgent transitions
We propose an extension to the formalism of timed automata by allowing urgent transitions. An urgent transition is a transition which must be taken within a fixed time interval from its enabling time and it ha...
-
Article
Logic Based Abstractions of Real-Time Systems
When verifying concurrent systems described by transition systems, state explosion is one of the most serious problems. If quantitative temporal information (expressed by clock ticks) is considered, state expl...
-
Chapter and Conference Paper
Formula Based Abstractions of Transition Systems for Real-Time Model Checking
When verifying concurrent systems described by transition systems, state explosion is one of the most serious problems. If quantitative temporal information (expressed by clock ticks) are considered,state expl...
-
Chapter
Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems
In model checking for temporal logic, the correctness of a (concurrent) system with respect to a desired behavior is verified by checking whether a structure that models the system satisfies a formula describi...
-
Chapter and Conference Paper
A multiple-valued logical semantics for Prolog
The coincidence of the declarative and procedural interpretations of logic programs does not apply to Prolog programs, due to the depth-first left-to-right evaluation strategy of Prolog interpreters. We propos...
-
Chapter and Conference Paper
Oracle semantics for Prologa
This paper proposes to specify semantic definitions for Prolog in terms of an oracle which provides information on which clauses are to be applied to resolve a given goal. The approach is quite general. It is ...
-
Chapter and Conference Paper
A tool to check the non-floundering logic programs and goals
A complete implementation of the negation as failure rule in a logic programming system requires that only ground negative literals are selected during the evaluation. Obviously there is the possibility to hav...
-
Chapter and Conference Paper
Intensional negation of logic programs: Examples and implementation techniques
Intensional negation is a transformation technique which, given the Horn clause definitions of a set of predicates pi, synthesizes the definitions of new predicates, pi∼ the meaning of which is the effective part...
