A Type System for Required/Excluded Elements in CLS (2009)
Dezani-Ciancaglini, Mariangiola, Giannini, Paola, Troina, Angelo
The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. We enrich this calculus with a type discipline to guarantee the...
Type Disciplines for Analysing Biologically Relevant Properties (2009)
Bogdan Aman, Mariangiola Dezani-ciancaglini, Angelo Troina
The calculus of looping sequences is a formalism for describing evolution of biological systems by means of term rewriting rules. We propose to enrich this calculus with type disciplines to guarantee...
MFPS 2008 Stochastic Bigraphs 1 (2009)
Jean Krivine, Robin Milner, Angelo Troina
In this paper we present a stochastic semantics for Bigraphical Reactive Systems. A reduction and a labelled stochastic semantics for bigraphs are defined. As a sanity check, we prove that the two...
Type Disciplines for Analysing Biologically Relevant Properties (2009)
Bogdan Aman, Mariangiola Dezani-ciancaglini, Angelo Troina
The calculus of looping sequences is a formalism for describing evolution of biological systems by means of term rewriting rules. We propose to enrich this calculus with type disciplines to guarantee...
Roberto Barbuti, Paolo Milazzo, Paolo Tiberi, Angelo Troina
Abstract. The paper presents the Stochastic Calculus of Looping Sequences (SCLS) suitable to describe microbiological systems, such as cellular pathways, and their evolution. Systems are represented...
Modelling an Ammonium Transporter with SCLS (2009)
Coppo, Mario, Damiani, Ferruccio, Grassi, Elena, Guether, Mike, Troina, Angelo
The Stochastic Calculus of Looping Sequences (SCLS) is a recently proposed modelling language for the representation and simulation of biological systems behaviour. It has been designed with the aim...
A Probabilistic Applied Pi–Calculus ⋆ (2009)
Jean Goubault-larrecq, Catuscia Palamidessi, Angelo Troina
Abstract. We propose an extension of the Applied Pi–calculus by introducing nondeterministic and probabilistic choice operators. The semantics of the resulting model, in which probability and...
IOS Press A Calculus of Looping Sequences for Modelling Microbiological Systems (2008)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
Abstract. The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent...
A Probabilistic Applied Pi–Calculus ⋆ (2008)
Jean Goubault-larrecq, Catuscia Palamidessi, Angelo Troina
Abstract. We propose an extension of the Applied Pi–calculus by introducing nondeterministic and probabilistic choice operators. The semantics of the resulting model, in which probability and...
IOS Press A Probabilistic Model for Molecular Systems (2008)
Roberto Barbuti, Stefano Cataudella, Paolo Milazzo C, Angelo Troina
Abstract. We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model and we show how a...
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. 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...
Angelo Troina, Alessandro Aldini, Roberto Gorrieri
We present a formal view of cryptography that overcomes the usual assumptions of formal models for reasoning about security of computer systems, i.e. perfect cryptography and Dolev-Yao adversary...
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
Abstract. We develop a model of Parametric Probabilistic Transition Systems, where probabilities associated with transitions may be parameters. We show how to find instances of the parameters that...
Verification of Hybrid Automata by Synthesis and Refinement (2008)
Ruggero Lanotte, Andrea Maggiolo-schettini, Simone Tini, Angelo Troina
Abstract. We present a verification technique to check properties of systems in the model of Linear Hybrid Automata. Given an automaton synthesized from a logic formula, we stepwise specialize...
Andrea Maggiolo-schettini, Angelo Troina
1 Introduction In a multilevel system every agent is confined in a bounded security level; information can flow from a certain agent to another agent only if the level of the former is lower than the...
IOS Press A Calculus of Looping Sequences for Modelling Microbiological Systems (2008)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
Abstract. The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent...
Angelo Troina, Alessandro Aldini, Roberto Gorrieri
We present a formal view of cryptography that overcomes the usual assumptions of formal models for reasoning about security of computer systems, i.e. perfect cryptography and Dolev-Yao adversary...
IOS Press A Probabilistic Model for Molecular Systems (2008)
Roberto Barbuti, Stefano Cataudella, Paolo Milazzo C, Angelo Troina
Abstract. We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a...
Probabilistic Timed Automata for Security Analysis and Design (2008)
Angelo Troina, Supervisor Prof, Andrea Maggiolo Schettini, Referee Prof, Catuscia Palamidessi, Referee Prof, ...
4 Abstract The usefulness of formal methods for the description and verification of complex systems is nowa-days widely accepted. While some system properties can be studied in a non-timed and...
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
Abstract. We develop a model of Parametric Probabilistic Transition Systems, where probabilities associated with transitions may be parameters. We show how to find instances of the parameters that...
A Probabilistic Applied Pi–Calculus ⋆ (2008)
Jean Goubault-larrecq, Catuscia Palamidessi, Angelo Troina
Abstract. We propose an extension of the Applied Pi–calculus by introducing nondeterministic and probabilistic choice operators. The semantics of the resulting model, in which probability and...
Verification of Hybrid Automata by Synthesis and Refinement (2008)
Ruggero Lanotte, Andrea Maggiolo-schettini, Simone Tini, Angelo Troina
Abstract. We present a verification technique to check properties of systems in the model of Linear Hybrid Automata. Given an automaton synthesized from a logic formula, we stepwise specialize...
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
Abstract. We develop a model of parametric probabilistic transition Systems (PPTSs), where probabilities associated with transitions may be parameters. We show how to find instances of the parameters...
Verification of Hybrid Automata by Synthesis and Refinement Ruggero Lanotte (2008)
Ruggero Lanotte, Simone Tini, Angelo Troina
We present a verification technique to check properties of systems in the model of Linear Hybrid Automata. Given an automaton synthesized from a logic formula, we stepwise specialize transitions and...
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Paolo Tiberi, Angelo Troina
Abstract. The paper presents the Stochastic Calculus of Looping Sequences (Stochastic CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed...
Design and Verification of Long–Running Transactions in a Timed Framework (2008)
Ruggero Lanotte, Andrea Maggiolo-Schettini, Paolo Milazzo, Angelo Troina
Long–running transactions consist of tasks which may be executed sequentially and in parallel, may contain sub–tasks, and may require to be completed before a deadline. These transactions are not...
A Probabilistic Applied Pi-Calculus (2007)
Goubault-Larrecq, Jean, Palamidessi, Catuscia, Troina, Angelo
We propose an extension of the Applied Picalculus by introducing nondeterministic and probabilistic choice operators. The semantics of the resulting model, in which probability and nondeterminism...
A Probabilistic Applied Pi-Calculus (2007)
Goubault-Larrecq, Jean, Palamidessi, Catuscia, Troina, Angelo
We propose an extension of the Applied Picalculus by introducing nondeterministic and probabilistic choice operators. The semantics of the resulting model, in which probability and nondeterminism...
The Calculus of Looping Sequences for Modeling Biological Membranes (2007)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
We survey the formalism Calculus of Looping Sequences (CLS) and a number of its variants from the point of view of their use for describing biological membranes. The formalism CLS is based on term...
The Calculus of Looping Sequences for Modeling Biological Membranes (2007)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
1 Introduction Cell biology, the study of the morphological and functional organization of cells,is now an established field in biochemical research. Computer Science can help the research in cell...
The Calculus of Looping Sequences for Modeling Biological Membranes (2007)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
Abstract. We survey the formalism Calculus of Looping Sequences (CLS) and a number of its variants from the point of view of their use for describing biological membranes. The formalism CLS is based...
The Calculus of Looping Sequences for Modeling Biological Membranes (2007)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
1 Introduction Cell biology, the study of the morphological and functional organization of cells,is now an established field in biochemical research. Computer Science can help the research in cell...
Definition of CLS CLS as an abstraction for biomolecular systems (2007)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
Outline of the talk
Probabilistic Timed Automata for Security Analysis and Design (2006)
The usefulness of formal methods for the description and verification of complex systems is nowadays widely accepted. While some system properties can be studied in a non-timed and non-probabilistic...
A Rewrite–based Formalism for Describing Biological Systems (2006)
Roberto Barbuti, Andrea Maggiolo Schettini, Paolo Milazzo, Angelo Troina
Formal models for systems of interactive components can be easily used or adapted for the modelling of biological phenomena Examples: Petri Nets, π–calculus, Mobile Ambients The modelling of...
Bisimulation Congruences in the Calculus of Looping Sequences (2006)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. The Calculus of Looping Sequences (CLS) is a calculus suitable to describe biological systems and their evolution. CLS terms are constructed by starting from basic constituents and...
Bisimulation Congruences in the Calculus of Looping Sequences (2006)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. The Calculus of Looping Sequences (CLS) is a calculus suitable to describe biological systems and their evolution. CLS terms are constructed by starting from basic constituents and...
Modeling Long-running Transactions with Communicating Hierarchical Timed Automata (2006)
Ruggero Lanotte, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. Long-running transactions consist of tasks which may be executed sequentially and in parallel, may contain sub-tasks, and may require to be completed before a deadline. These transactions...
Bisimulation Congruences in the Calculus of Looping Sequences (2006)
Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, Angelo Troina
The Calculus of Looping 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...
A Calculus of Looping Sequences for Modelling Microbiological Systems (2006)
Roberto Barbuti, Andrea Maggiolo--Schettini, Paolo Milazzo, Angelo Troina
The paper presents the Calculus of Looping Sequences (CLS) suitable to describe microbiological systems and their evolution. The terms of the calculus are constructed by basic constituent elements...
Modeling Long--Running Transactions with (2006)
Communicating Hierarchical Timed, Ruggero Lanotte, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Long-Running transactions consist of tasks which may be executed sequentially and in parallel, may contain sub-tasks, and may require to be completed before a deadline. These transactions are not...
Bisimulation Congruences in the Calculus of Looping Sequences (2006)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. The Calculus of Looping Sequences (CLS) is a calculus suitable to describe biological systems and their evolution. CLS terms are constructed by starting from basic constituents and...
A Calculus of Looping Sequences for Modelling Microbiological Systems (2006)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. The paper presents a new calculus suitable to describe microbiological systems and their evolution. We use the calculus to model interactions among bacteria and bacteriophage viruses, and...
Modeling Long-running Transactions with Communicating Hierarchical Timed Automata (2006)
Ruggero Lanotte, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. Long-Running transactions consist of tasks which may be executed sequentially and in parallel, may contain sub-tasks, and may require to be completed before a deadline. These transactions...
Bisimulation Congruences in the Calculus of Looping Sequences (2006)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. The Calculus of Looping Sequences (CLS) is a calculus suitable to describe biological systems and their evolution. CLS terms are constructed by starting from basic constituents and...
A Calculus of Looping Sequences for Modelling Microbiological Systems (2006)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. The paper presents a new calculus suitable to describe microbiological systems and their evolution. We use the calculus to model interactions among bacteria and bacteriophage viruses, and...
Modeling Long-running Transactions with Communicating Hierarchical Timed Automata (2006)
Ruggero Lanotte, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
1 Introduction The term transaction is commonly used in database systems to denote a logi-cal unit of work designed for short-lived activities, usually lasting under a few
Prof Catuscia Palamidessi, Angelo Troina, Prof Andrea, Maggiolo Schettini, Prof Christel Baier
incoraggiamenti, i suoi consigli e la sua amicizia sono sempre stati preziosi. Andrea, grazie per quanto hai fatto in questi anni, è veramente un piacere lavorare con te. Il supporto e il contributo...
Probabilistic Timed Automata for Security Analysis and Design (2006)
Angelo Troina, Prof Andrea, Maggiolo Schettini
The usefulness of formal methods for the description and verification of complex systems is nowadays widely accepted. While some system properties can be studied in a non-timed and nonprobabilistic...
The Java Virtual Machine Specification, http://java.sun.com/docs/books/vmspec (2005)
Angelo Troina, Ro Aldini, Roberto Gorrieri
Abstract. Polynomial time adversaries based on a computational view of cryptography have additional capabilities that the classical Dolev-Yao adversary model does not include. To relate these two...
An alternative to Gillespie’s algorithm for simulating chemical reactions (2005)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
Abstract. We introduce a probabilistic algorithm for the simulation of chemical reactions, which can be used as an alternative to the wellestablished stochastic algorithm proposed by D.T. Gillespie...
A Probabilistic Model for Molecular Systems (2005)
Roberto Barbuti, Stefano Cataudella, Andrea Maggiolo-Schettini, Paolo Milazzo, And Angelo Troina, Angelo Troina
We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a...
A Classification of Time and/or Probability Dependent Security Properties (2005)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow...
An Alternative to Gillespie's Algorithm for Simulating Chemical Reactions (2005)
Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, And Angelo Troina, Angelo Troina
We introduce a probabilistic algorithm for the simulation of chemical reactions, which can be used as an alternative to the wellestablished stochastic algorithm proposed by D.T. Gillespie in the...
A Calculus of Looping Sequences For Modelling Microbiological Systems (2005)
Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, And Angelo Troina, Angelo Troina
The paper presents a new calculus suitable to describe microbiological systems and their evolution. We use the calculus to model interactions among bacteria and bacteriophage viruses, and to reason...
Towards a Formal Treatment of Secrecy against Computational Adversaries (2005)
Angelo Troina, Alessandro Aldini, Ro Aldini, Roberto Gorrieri
Polynomial time adversaries based on a computational view of cryptography have additional capabilities that the classical Dolev-Yao adversary model does not include. To relate these two di#erent...
QAPL 2005 Preliminary Version (2005)
Classification Of Time, Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow...
An alternative to Gillespie’s algorithm for simulating chemical reactions (2005)
Roberto Barbuti, Paolo Milazzo, Angelo Troina
Abstract. We introduce a probabilistic algorithm for the simulation of chemical reactions, which can be used as an alternative to the wellestablished stochastic algorithm proposed by D.T. Gillespie...
An alternative to Gillespie’s algorithm for simulating chemical reactions (2005)
Roberto Barbuti, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. We introduce a probabilistic algorithm for the simulation of chemical reactions, which can be used as an alternative to the wellestablished stochastic algorithm proposed by D.T. Gillespie...
A Classification of Time and/or Probability Dependent Security (2005)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow...
The Java Virtual Machine Specification, http://java.sun.com/docs/books/vmspec (2005)
Angelo Troina, Ro Aldini, Roberto Gorrieri
Abstract. Polynomial time adversaries based on a computational view of cryptography have additional capabilities that the classical Dolev-Yao adversary model does not include. To relate these two...
The Java Virtual Machine Specification, http://java.sun.com/docs/books/vmspec (2005)
Angelo Troina, Ro Aldini, Roberto Gorrieri
Abstract. Polynomial time adversaries based on a computational view of cryptography have additional capabilities that the classical Dolev-Yao adversary model does not include. To relate these two...
Troina: Information Flow Analysis for Probabilistic Timed Automata (2004)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
Abstract In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information...
Information Flow Analysis for Probabilistic Timed Automata (2004)
Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina
In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information flow...
Automatic Covert Channel Analysis of a Multilevel Secure Component (2004)
Ruggero Lanotte, Andrea Maggiolo-Schettini, Simone Tini, Angelo Troina, Enrico Tronci
The NRL Pump protocol defines a multilevel secure component whose goal is to minimize leaks of information from high level systems to lower level systems, without degrading average time performances.
Automatic Analysis of the NRL Pump (2004)
Ruggero Lanotte, Andrea Maggiolo-Schettini, Simone Tini, Angelo Troina, Enrico Tronci
We define a probabilistic model for the NRL Pump and using FHP-murφ show experimentally that there exists a probabilistic covert channel whose capacity depends on various NRL Pump parameters (e.g....
Automatic Analysis of a Non-Repudiation Protocol (2004)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
We define a probabilistic model for the analysis of a Non-Repudiation protocol that guarantees fairness, without resorting to a trusted third party, by means of a probabilistic algorithm. By using...
Automatic Analysis of a Non-Repudiation Protocol (2004)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
We define a probabilistic model for the analysis of a Non-Repudiation protocol that guarantees fairness, without resorting to a trusted third party, by means of a probabilistic algorithm. By using...
Automatic Analysis of a Non-Repudiation Protocol (2004)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
We define a probabilistic model for the analysis of a Non-Repudiation protocol that guarantees fairness, without resorting to a trusted third party, by means of a probabilistic algorithm. By using...
Troina: Information Flow Analysis for Probabilistic Timed Automata (2004)
Ruggero Lanotte, Angelo Troina
Abstract In multilevel systems it is important to avoid unwanted indirect information flow from higher levels to lower levels, namely the so called covert channels. Initial studies of information...
Automatic Covert Channel Analysis of a Multilevel Secure Component (2004)
Ruggero Lanotte, Andrea Maggiolo-schettini, Simone Tini, Angelo Troina, Enrico Tronci
A probabilistic calculus for molecular systems (2004)
Roberto Barbuti, Stefano Cataudella, Andrea Maggiolo-schettini, Paolo Milazzo, Angelo Troina
Abstract. We introduce a calculus for molecular reactions based on probabilistic rules. On the one hand, according to the semantics of the rules, we give an interpreter to study the behaviour of...
Automatic Covert Channel Analysis of a Multilevel Secure Component (2004)
Ruggero Lanotte, Andrea Maggiolo-schettini, Simone Tini, Angelo Troina, Enrico Tronci
Abstract. The NRL Pump protocol defines a multilevel secure component whose goal is to minimize leaks of information from high level systems to lower level systems, without degrading average time...
A Probabilistic Formulation of Imperfect Cryptography (2003)
Angelo Troina, Alessandro Aldini, Ro Aldini, Roberto Gorrieri
We present a novel equivalence for cryptographic expressions that overcomes two limitations of classical security models: perfect cryptography and nondeterministic adversary. The uncertainty...
Weak Bisimulation for Probabilistic Timed Automata (2003)
And Applications To, Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
We are interested in describing timed systems that exhibit probabilistic behaviors. To this purpose, we define a model of probabilistic timed automata and give a concept of weak bisimulation together...
Approximating Imperfect Cryptography in a Formal Model (2003)
Angelo Troina, Alessandro Aldini, Roberto Gorrieri
We present a formal view of cryptography that overcomes the usual assumptions of formal models for reasoning about security of computer systems, i.e. perfect cryptography and Dolev-Yao adversary...
A Probabilistic Formulation of Imperfect Cryptography (2003)
Angelo Troina, Ro Aldini, Roberto Gorrieri
Abstract. We present a novel equivalence for cryptographic expressions that overcomes two limitations of classical security models: perfect cryptography and nondeterministic adversary. The...
Weak Bisimulation for Probabilistic Timed Automata and Applications to Security (2003)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
We are interested in describing timed systems that exhibit probabilistic behaviors. To this purpose, we define a model of probabilistic timed automata and give a concept of weak bisimulation together...
Weak Bisimulation for Probabilistic Timed Automata and Applications to Security (2003)
Ruggero Lanotte, Andrea Maggiolo-schettini, Angelo Troina
We are interested in describing timed systems that exhibit probabilistic behaviors. To this purpose, we define a model of probabilistic timed automata and give a concept of weak bisimulation together...
A Probabilistic Formulation of Imperfect Cryptography (2003)
Angelo Troina, Ro Aldini, Roberto Gorrieri
Abstract. We present a novel equivalence for cryptographic expressions that overcomes two limitations of classical security models: perfect cryptography and nondeterministic adversary. The...