Search

Model checking is an effective way to design correct software. Making behavioural models of software, formulating correctness properties using modal formulas, and verifying these using finite state analysis techniques, is a very efficient way to obtain the required insight in the software. We illustrate this on four common but tricky examples.

The notion of bisimulation as proposed by Larsen and Skou for discrete probabilistic transition systems is shown to coincide with a coalgebraic definition in the sense of Aczel and Mendler in terms of a set functor, which associates to a set its collection of simple probability distributions. This coalgebraic formulation makes it possible to generalize the concepts of discrete probabilistic transition system and probabilistic bisimulation to a continuous setting involving Borel probability measures. A functor ℳ1 is introduced that yields for a metric space its collection of Borel probability measures. Under reasonable conditions, this functor exactly captures generalized probabilistic bisimilarity. Application of the final coalgebra paradigm to a functor based on ℳ1 then yields an internally fully abstract semantical domain with respect to probabilistic bisimulation, which is therefore well suited for the interpretation of probabilistic specification and stochastic programming concepts.

Contains fulltext : 60368.pdf (Publisher’s version ) (Closed access)

We show in a uniform setting the crucial role of compactness in the theory of the Smyth powerdomain of streams. The topological notion of compactness is characterized in an order- theoretical manner, involving a notion of bounded sets. We obtain general results on the continuity of operators, and consider applications as diverse as interleaving, hiding and stream programming operators.

We show in a uniform setting the crucial role of compactness in the theory of the Smyth powerdomain of streams. The topological notion of compactness is characterized in an order-theoretical manner, involving a notion of bounded sets. We obtain general results on the continuity of operators, and consider applications as diverse as interleaving, hiding and stream programming operators.

QFLan offers modeling and analysis of highly reconfigurable systems, like product lines, which are characterized by combinatorially many system variants (or products) that can be obtained via different combinations of installed features. The tool offers a modern integrated development environment for the homonym probabilistic feature-oriented language. QFLan allows the specification of a family of products in terms of a feature model with quantitative attributes, which defines the valid feature combinations, and probabilistic behavior subject to quantitative constraints. The language's behavioral part enables dynamic installation, removal and replacement of features. QFLan has a discrete-time Markov chain semantics, permitting quantitative analyses. Thanks to a seamless integration with the statistical model checker MultiVeStA, it allows for analyses like the likelihood of specific behavior or the expected average value of non-functional aspects related to feature attributes.

In this paper we propose a systematic approach to construct mathematical models describing populations of cancer-cells at different stages of disease development. The methodology we propose is based on stochastic Concurrent Constraint Programming, a flexible stochastic modelling language. The methodology is tested on (and partially motivated by) the study of prostate cancer. In particular, we prove how our method is suitable to systematically reconstruct different mathematical models of prostate cancer growth - together with interactions with different kinds of hormone therapy - at different levels of refinement., In Proceedings CompMod 2011, arXiv:1109.1044

We give an overview of recent work on the rule-based modeling of nano devices. In particular, our experience in the modeling of a nanoscale elevator suggested us to enhance rule-based modeling with complex functional rates that can be used to express rates that depend on the current state of the entire complexes in which the reacting molecules reside.