Search

We treat the problem of generating cost-optimal schedules for orders with individual due dates and cost functions based on earliness/tardiness. Orders can run in parallel in a resource-constrained manufacturing environment, where resources are subject to stochastic breakdowns. The goal is to generate schedules while minimizing the expected costs. First, we estimate the distribution of each order type by simulation (assuming a reasonable machine/load model) and derive from the cost-function an optimal offset from the due date of each individual order. Second, these optimal offsets are then used to guide the generation of schedules which are responsible to resolve resource conflicts. Third, we evaluate the generated schedules by simulation. The approach is demonstrated by means of a non-trivial case-study from lacquer production. Optimal offsets are derived with the Modest/Möbius tool, schedules are generated using Uppaal Cora. The experimental results show that our approach achieves good results in all considered scenarios, and better results than an approach based on adding slack to processing times.

This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.

Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.

This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.

Markov chains are widely used in the context of the performance and reliability modeling of various systems. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both discrete [34, 10] and continuous time settings [7, 12]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker EIMC2, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore, we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of EIMC2.

Markov chains (and their extensions with rewards) have been widely used to determine performance, dependability and performability characteristics of computer communication systems, such as throughput, delay, mean time to failure, or the probability to accumulate at least a certain amount of reward in a given time. Due to the rapidly increasing size and complexity of systems, Markov chains and Markov reward models are difficult and cumbersome to specify by hand at the state-space level. Therefore, various specification formalisms, such as stochastic Petri nets and stochastic process algebras, have been developed to facilitate the specification of these models at a higher level of abstraction. Up till now, however, the specification of the measure-of-interest is often done in an informal and relatively unstructured way. Furthermore, some measures-of-interest can not be expressed conveniently at all. In this tutorial paper, we present a logic-based specification technique to specify performance, dependability and performability measures-of-interest and show how for a given finite Markov chain (or Markov reward model) such measures can be evaluated in a fully automated way. Particular emphasis will be given to so-called path-based measures and hierarchically-specified measures. For this purpose, we extend so-called model checking techniques to reason about discrete- and continuous-time Markov chains and their rewards. We also report on the use of techniques such as (compositional) model reduction and measure-driven state-space generation to combat the infamous state space explosion problem.

This paper proposes a partial-order semantics for a stochastic process algebra that supports general (non-memoryless) distributions and combines this with an approach to numerically analyse the first passage time of an event. Based on an adaptation of McMillan's complete finite prefix approach tailored to event structures and process algebra, finite representations are obtained for recursive processes. The behaviour between two events is now captured by a partial order that is mapped on a stochastic task graph, a structure amenable to numerical analysis. Our approach is supported by the (new) tool Forest for generating the complete prefix and the (existing) tool Pepp for analysing the generated task graph. As a case study, the delay of the first resolution in the root contention phase of the IEEE 1394 serial bus protocol is analysed. 1

Over the last two decades formal methods have been extended towards performance and reliability evaluation. This paper tries to provide a rather intuitive explanation of the basic concepts and features in this area. Instead of striving for mathematical rigour, the intention is to give an illustrative introduction to the basics of stochastic models, to stochastic modelling using process algebra, and to model checking as a technique to analyse stochastic models.

The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branching-time temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form \({\cal P}_{\bowtie p}(\Phi_1 \, {\cal U}^{I} \, \Phi_2)\), for state formulas Φ1 and Φ2, comparison operator ⋈, probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.

A major reason for studying probabilistic processes is to establish a link between a formal model for describing functional system behaviour and a stochastic process. Compositionality is an essential ingredient for specifying systems. Parallel composition in a probabilistic setting is complicated since it gives rise to non-determinism, for instance due to interleaving of independent autonomous activities. This paper presents a detailed study of the resolution of non-determinism in an asynchronous generative setting. Based on the intuition behind the synchronous probabilistic calculus PCCS we formulate two criteria that an asynchronous parallel composition should fulfill. We provide novel probabilistic variants of parallel composition for CCS and CSP and show that these operators satisfy these general criteria, opposed to most existing proposals. Probabilistic bisimulation is shown to be a congruence for these operators and their expansion is addressed. We would like to thank the reviewers for their constructive criticism and for pointing out the relation between BPTSs and the model of Pnueli and Zuck. We also thank Ed Brinksma and Rom Langerak (both of the University of Twente) for fruitful discussions.

During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi. During the last decade, CCS has been extended in different directions, among them priority and real time. One of the most satisfactory results for CCS is Milner's complete proof system for observational congruence [28]. Observational congruence is fair in the sense that it is possible to escape divergence, reflected by an axiom recX.(Τ.X + P)=recX.Τ.P. In this paper we discuss observational congruence in the context of interactive Markov chains, a simple stochastic timed variant CCS with maximal progress. This property implies that observational congruence becomes unfair, i.e. it is not always possible to escape divergence. This problem also arises in calculi with priority. So, completeness results for such calculi modulo observational congruence have been unknown until now. We obtain a complete proof system by replacing the above axiom by a set of axioms allowing to escape divergence by means of a silent alternative. This treatment can be profitably adapted to other calculi.

This paper presents a novel linear process-algebraic format for probabilistic automata. The key ingredient is a symbolic transformation of probabilistic process algebra terms that incorporate data into this linear format while preserving strong probabilistic bisimulation. This generalises similar techniques for traditional process algebras with data, and — more importantly — treats data and data-dependent probabilistic choice in a fully symbolic manner, paving the way to the symbolic analysis of parameterised probabilistic systems.

This dissertation considers three important aspects of model checking Markov models: diagnosis — generating counterexamples, synthesis — providing valid parameter values and analysis — verifying linear real-time properties. The three aspects are relatively independent while all contribute to developing new theory and algorithms in the research field of probabilistic model checking. We start by introducing a formal definition of counterexamples in the setting of probabilistic model checking. We transform the problem of finding informative counterexamples to shortest path problems. A framework is explored and provided for generating such counterexamples. We then investigate a more compact representation of counterexamples by regular expressions. Heuristic based algorithms are applied to obtain short regular expression counterexamples. In the end of this part, we extend the definition and counterexample generation algorithms to various combinations of probabilistic models and logics. We move on to the problem of synthesizing values for parametric continuous-time Markov chains (pCTMCs) wrt. time-bounded reachability specifications. The rates in the pCTMCs are expressed by polynomials over reals with parameters and the main question is to find all the parameter values (forming a synthesis region) with which the specification is satisfied. We first present a symbolic approach where the intersection points are computed by solving polynomial equations and then connected to approximate the synthesis region. An alternative non-symbolic approach based on interval arithmetic is investigated, where pCTMCs are instantiated. The error bound, time complexity as well as some experimental results have been provided, followed by a detailed comparison of the two approaches. In the last part, we focus on verifying CTMCs against linear real-time properties specified by deterministic timed automata (DTAs). The model checking problem aims at computing the probability of the set of paths in CTMC C that can be accepted by DTA A, denoted PathsC(A). We consider DTAs with reachability (finite, DTA♦) and Muller (infinite, DTAω) acceptance conditions, respectively. It is shown that PathsC(A) is measurable and computing its probability for DTA♦ can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of PDEs. Furthermore, we show that the special case of single-clock DTA♦ can be simplified to solving a system of linear equations. We also deal with DTAω specifications, where the problem is proven to be reducible to the reachability problem as in the DTA♦ case.

Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulae in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that typically the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol.

We study the following problem: given a continuous-time Markov chain (CTMC) C, and a linear real-time property provided as a deterministic timed automaton (DTA) A, what is the probability of the set of paths of C that are accepted by A (C satisfies A)? It is shown that this set of paths is measurable and computing its probability can be reduced to computing the reachability probability in a piecewise deterministic Markov process (PDP). The reachability probability is characterized as the least solution of a system of integral equations and is shown to be approximated by solving a system of partial differential equations. For the special case of single-clock \DTA, the system of integral equations can be transformed into a system of linear equations where the coefficients are solutions of ordinary differential equations.

A continuous-time Markov decision process (CTMDP) is a generalization of a continuous-time Markov chain in which both probabilistic and nondeterministic choices co-exist. This paper presents an efficient algorithm to compute the maximum (or minimum) probability to reach a set of goal states within a given time bound in a uniform CTMDP, i.e., a CTMDP in which the delay time distribution per state visit is the same for all states. We prove that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way. This work is supported by the NWO-DFG bilateral project Validation of Stochastic Systems.

Models used for the analysis of dependability and performance attributes of communication protocols often abstract considerably from the details of the actual protocol. These models often consist of concurrent sub-models and this may make it hard to judge whether their behaviour is faithfully reflecting the protocol. In this paper, we show how model checking of continuous-time Markov chains, generated from high-level specifications, facilitates the analysis of both correctness and dependability attributes. We illustrate this by revisiting a dependability analysis [Analysis and estimation of the quality of service of group communication protocols] of a variant of the central access protocol of the IEEE 802.11 standard for wireless local area networks. This variant has been developed to support real-time group communication between autonomous mobile stations. Correctness and dependability properties are formally characterised using Continuous Stochastic Logic and are automatically verified by the ETMCC model checker. The models used are specified as Stochastic Activity Nets.

This paper considers a weak simulation preorder for Markov chains that allows for stuttering. Despite the second-order quantification in its definition, we present a polynomial-time algorithm to compute the weak simulation preorder of a finite Markov chain.

This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.

This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterised in terms of the temporal logics PCTL and CSL. Apart from presenting various existing branching-time relations in a uniform manner, our contributions are: (i) weak simulation for DTMCs is defined, (ii) weak bisimulation equivalence is shown to coincide with weak simulation equivalence, (iii) logical characterisation of weak (bi)simulations are provided, and (iv) a classification of branching-time relations is presented, elucidating the semantics of DTMCs, CTMCs and their interrelation.

This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

Invited Contributions.- Failure Detection vs Group Membership in Fault-Tolerant Distributed Systems: Hidden Trade-Offs.- Probability and Timing: Challenges for Secure Programming.- Selected Papers.- Security Analysis of a Probabilistic Non-repudiation Protocol.- The Mean Value of the Maximum.- Reduction and Refinement Strategies for Probabilistic Analysis.- Action Refinement for Probabilistic Processes with True Concurrency Models.- Probabilistic Unfoldings and Partial Order Fairness in Petri Nets.- Possibilistic and Probabilistic Abstraction-Based Model Checking.- Out-of-Core Solution of Large Linear Systems of Equations Arising from Stochastic Modelling.- Model Checking CSL until Formulae with Random Time Bounds.- Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol.- Deriving Symbolic Representations from Stochastic Process Algebras.- Short Abstracts.- A Generalization of Equational Proof Theory?.- An Integrated Approach for the Specification and Analysis of Stochastic Real-Time Systems.- Probabilistic Abstract Interpretation and Statistical Testing.- Approximate Verification of Probabilistic Systems.

This paper surveys the theoretical developments in the field of stochastic process algebras, process algebras where action occurrences may be subject to a delay that is determined by a random variable. A huge class of resource-sharing systems – like large-scale computers, client–server architectures, networks – can accurately be described using such stochastic specification formalisms. The main emphasis of this paper is the treatment of operational semantics, notions of equivalence, and (sound and complete) axiomatisations of these equivalences for different types of Markovian process algebras, where delays are governed by exponential distributions. Starting from a simple actionless algebra for describing time-homogeneous continuous-time Markov chains, we consider the integration of actions and random delays both as a single entity (like in known Markovian process algebras like TIPP, PEPA and EMPA) and as separate entities (like in the timed process algebras timed CSP and TCCS). In total we consider four related calculi and investigate their relationship to existing Markovian process algebras. We also briefly indicate how one can profit from the separation of time and actions when incorporating more general, non-Markovian distributions.

This paper surveys and relates the basic concepts of process algebra and the modelling of continuous time Markov chains. It provides basic introductions to both fields, where we also study the Markov chains from an algebraic perspective, viz. that of Markov chain algebra. We then proceed to study the interrelation of reactive processes and Markov chains in this setting, and introduce the algebra of Interactive Markov Chains as an orthogonal extension of both process and Markov chain algebra. We conclude with comparing this approach to related (Markovian) stochastic process algebras by analysing the algebraic principles that they support.

Real-time, performance and reliability aspects are of vital importance in the entire system design trajectory. Therefore, modelling techniques are needed that cover quantitative system aspects. This paper presents MoDeST, a modelling language that allows us to specify soft real-time constraints (i.e., stochastic timing) as well as hard real-time constraints. MoDeST combines conventional programming constructs – such as iteration, alternatives, atomic statements, and exception handling – with means to describe complex systems in a compositional manner. The language is influenced by popular and user-friendly specification languages, and deals with compositionality in a light-weight process-algebra style. In summary, MoDeST (i) covers a very broad spectrum of modelling concepts, (ii) possesses a rigid, process-algebra style semantics, and (iii) yet provides modern and flexible specification constructs.

Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-in terest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.

This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.

Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [8] and the continuous time setting [1], [3]. In this short paper, we describe the prototype model checker $E \vdash M C^2$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.

Over the last two decades formal methods have been extended towards performance and reliability evaluation. This paper tries to provide a rather intuitive explanation of the basic concepts and features in this area. Instead of striving for mathematical rigour, the intention is to give an illustrative introduction to the basics of stochastic models, to stochastic modelling using process algebra, and to model checking as a technique to analyse stochastic models.

Real-time, performance and reliability aspects are of vital importance in the entire system design trajectory. Therefore, modelling techniques are needed that cover quantitative system aspects. This paper presents MoDeST, a modelling language that allows us to specify soft real-time constraints (i.e., stochastic timing) as well as hard real-time constraints. MoDeST combines conventional programming constructs – such as iteration, alternatives, atomic statements, and exception handling – with means to describe complex systems in a compositional manner. The language is influenced by popular and user-friendly specification languages, and deals with compositionality in a light-weight process-algebra style. In summary, MoDeST (i) covers a very broad spectrum of modelling concepts, (ii) possesses a rigid, process-algebra style semantics, and (iii) yet provides modern and flexible specification constructs.

We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.

Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.

We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.

Stochastic process algebras have been proven useful because they allow behaviour-oriented performance and reliability modelling. As opposed to traditional performance modelling techniques, the behaviour- oriented style supports composition and abstraction in a natural way. However, analysis of stochastic process algebra models is state-oriented, because standard numerical analysis is typically based on the calculation of (transient and steady) state probabilities. This shift of paradigms hampers the acceptance of the process algebraic approach by performance modellers. In this paper, we develop an entirely behaviour-oriented analysis technique for stochastic process algebras. The key contribution is an action-based temporal logic to describe behaviours-of-interest, together with a model checking algorithm to derive the probability with which a stochastic process algebra model exhibits a given behaviour-of-interest.

Stochastic process algebras have been proven useful because they allow behaviour-oriented performance and reliability modelling. As opposed to traditional performance modelling techniques, the behaviour- oriented style supports composition and abstraction in a natural way. However, analysis of stochastic process algebra models is state-oriented, because standard numerical analysis is typically based on the calculation of (transient and steady) state probabilities. This shift of paradigms hampers the acceptance of the process algebraic approach by performance modellers. In this paper, we develop an entirely behaviour-oriented analysis technique for stochastic process algebras. The key contribution is an action-based temporal logic to describe behaviours-of-interest, together with a model checking algorithm to derive the probability with which a stochastic process algebra model exhibits a given behaviour-of-interest.

We present a translation from stochastic automata [17, 16] into timed automata with deadlines [37, 13]. The translation preserves traces when the stochastic characteristics, namely the probability measures, are abstracted from the original stochastic automaton. Moreover, we show that the translation is compositional in the sense that the translation of the parallel composition of two stochastic automata is equivalent to the parallel composition of the timed automata resulting from the translation of each stochastic automaton. The translation aims to borrow techniques and tools successfully developed in the context of timed automata and apply them to analyse the correctness of systems modelled in terms of stochastic automata.

We present a translation from stochastic automata [17, 16] into timed automata with deadlines [37, 13]. The translation preserves traces when the stochastic characteristics, namely the probability measures, are abstracted from the original stochastic automaton. Moreover, we show that the translation is compositional in the sense that the translation of the parallel composition of two stochastic automata is equivalent to the parallel composition of the timed automata resulting from the translation of each stochastic automaton. The translation aims to borrow techniques and tools successfully developed in the context of timed automata and apply them to analyse the correctness of systems modelled in terms of stochastic automata.

Markov-reward models, as extensions of continuous-time Markov chains, have received increased attention for the specification and evaluation of performance and dependability properties of systems. Until now, however, the specification of reward-based performance and dependability measures has been done manually and informally. In this paper, we change this undesirable situation by the introduction of a continuous-time, reward-based stochastic logic. We argue that this logic is adequate for expressing performability measures of a large variety. We isolate two important sub-logics, the logic CSL [#!ASS+96!#,#!BKH99!#], and the novel logic CRL that allows one to express reward-based properties. These logics turn out to be complementary, which is formally established in our main duality theorem. This result implies that reward-based properties expressed in CRL for a particular Markov reward model can be interpreted as CSL properties over a derived continuo us-time Markov chain, so that model checking procedures for CSL [#!BKH99!#,#!BHHK00!#] can be employed.

Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.

Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.

In this short paper we briefly describe a tool which is based on a Markovian stochastic process algebra. The tool offers both model specification and quantitative model analysis in a compositional fashion, wrapped in a userfriendly graphical front-end.

Stochastic process algebras have been introduced in order to enable compositional performance analysis. The size of the state space is a limiting factor, especially if the system consists of many cooperating components. To fight state space explosion, various proposals for compositional aggregation have been made. They rely on minimisation with respect to a congruence relation. This paper addresses the computational complexity of minimisation algorithms and explains how efficient, BDD-based data structures can be employed for this purpose.

Stochastic process algebras have been introduced in order to enable compositional performance analysis. The size of the state space is a limiting factor, especially if the system consists of many cooperating components. To fight state space explosion, various proposals for compositional aggregation have been made. They rely on minimisation with respect to a congruence relation. This paper addresses the computational complexity of minimisation algorithms and explains how efficient, BDD-based data structures can be employed for this purpose.

In this short paper we briefly describe a tool which is based on a Markovian stochastic process algebra. The tool offers both model specification and quantitative model analysis in a compositional fashion, wrapped in a userfriendly graphical front-end.