Page
%P
44 Result(s)
within
Roberto Bruni
Software Engineering/Programming and Operating Systems
-
Article
Open AccessCausal analysis of positive Reaction Systems
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 someh...
-
Chapter and Conference Paper
Exploiting Adjoints in Property Directed Reachability Analysis
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-...
-
Chapter
Verification of Reaction Systems Processes
Reaction Systems (RSs) are a computational framework inspired by biological systems. A RS is formed by a set of entities together with a set of reactions over them. Entities can enable or inhibit each reaction...
-
Chapter
Local Completeness in Abstract Interpretation
Completeness of an abstract interpretation is an ideal situation where the abstract interpreter is guaranteed to be compositional and producing no false alarm when used for verifying program correctness. Compl...
-
Chapter and Conference Paper
Exploiting Modularity of SOS Semantics to Define Quantitative Extensions of Reaction Systems
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 reacti...
-
Chapter
Petri Inheritance: The Foundation of Nondeterministic, Concurrent Systems
The personal contacts of the first author with Carl Adam Petri and Petri nets are initially described and the role of Petri nets as a connector algebra is then examined.
-
Chapter
Enhancing Reaction Systems: A Process Algebraic Approach
In the area of Natural Computing, reaction systems are a qualitative abstraction inspired by the functioning of living cells, suitable to model the main mechanisms of biochemical reactions. This model has alre...
-
Chapter
A Coalgebraic Approach to Unification Semantics of Logic Programming
In the version of logic programming (LP) based on interpretations where variables occur in atoms, a goal reduction via unification can be seen as a transition labelled by the most general unifier. Categoricall...
-
Book
-
Chapter
PEPA - Performance Evaluation Process Algebra
The probabilistic and stochastic models we have presented in previous chapters represent system behaviour but not its structure, i.e., they take a monolithic view and do not make explicit how the system is com...
-
Chapter
Preliminaries
In this chapter we fix some basic mathematical notation used in the rest of the book and introduce the important concepts of signature, logical system and goal-oriented derivation.
-
Chapter
Domain Theory
As we have done for IMP, we would like to introduce the denotational semantics of HOFL, for which we need to develop a proper domain theory that is more sophisticated than the one presented in Chapter 5. In or...
-
Chapter
Discrete Time Markov Chains with Actions and Nondeterminism
In this chapter we introduce some advanced probabilistic models that can be defined by enriching the transition functions of PTSs. As we have seen for Markov chains, the transition system representation is ver...
-
Chapter
Operational Semantics of IMP
This chapter introduces the formal syntax and operational semantics of a simple, structured imperative language called IMP, with static variable allocation and no sophisticated declaration constructs for data ...
-
Chapter
Partial Orders and Fixpoints
This chapter is devoted to the introduction of the foundations of the denotational semantics of computer languages. The concepts of complete partial orders with bottom and of monotone and continuous functions ...
-
Chapter
Operational Semantics of HOFL
In the previous part of the book we have introduced and studied an imperative language called IMP. In this chapter we move our attention to functional languages. In particular, we introduce HOFL, a simple high...
-
Chapter
Denotational Semantics of HOFL
In this chapter we exploit the domain theory from Chapter 8 to define the (lazy) denotational semantics of HOFL. For each type τ we introduce a corresponding domain (V τ ...
-
Chapter
Equivalence Between HOFL Denotational and Operational Semantics
In this chapter we address the correspondence between the operational semantics of HOFL from Chapter 7 and its denotational semantics from Chapter 9. The situation is not as straightforward as for IMP. A first...
-
Chapter
Temporal Logic and the μ-Calculus
As we have briefly discussed in the previous chapter, modal logic is a powerful tool that allows us to check important behavioural properties of systems. In Section 11.6 the focus was on Hennessy-Milner logic,...
-
Chapter
Measure Theory and Markov Chains
The future is largely unpredictable. Nondeterminism allows modelling of some phenomena arising in reactive systems, but it does not allow a quantitative estimation of how likely is one event w.r.t. another.We ...
