In the past, logics of several kinds have been proposed for reasoning about discrete-time or continuous-time Markov chains. Most of these logics rely on either state labels (atomic propositions) or on transition labels (actions). However, in several applications it is useful to reason about both state properties and action sequences. For this purpose, we introduce the logic as CSL which provides a powerful means to characterize execution paths of Markov chains with actions and state labels. asCSL can be regarded as an extension of the purely state-based logic CSL (continuous stochastic logic). In asCSL, path properties are characterized by regular expressions over actions and state formulas. Thus, the truth value of path formulas depends not only on the available actions in a given time interval, but also on the validity of certain state formulas in intermediate states. We compare the expressive power of CSL and asCSL and show that even the state-based fragment of asCSL is strictly more expressive than CSL if time intervals starting at zero are employed. Using an automaton-based technique, an asCSL formula and a Markov chain with actions and state labels are combined into a product Markov chain. For time intervals starting at zero, we establish a reduction of the model checking problem for asCSL to CSL model checking on this product Markov chain. The usefulness of our approach is illustrated with an elaborate model of a scalable cellular communication system, for which several properties are formalized by means of asCSL formulas and checked using the new procedure

In this paper we introduce the logic asCSL, an extension of continuous stochastic logic (CSL), which provides powerful means to characterise execution paths of action- and state-labelled Markov chains. In asCSL, path properties are characterised by regular expressions over actions and state-formulas. Thus, the executability of a path not only depends on the available actions but also on the validity of certain state formulas in intermediate states. Our main result is that the model checking problem for asCSL can be reduced to CSL model checking on a modified Markov chain, which is obtained through a product automaton construction. We provide a case study of a scalable cellular phone system which shows how the logic asCSL and the model checking procedure can be applied in practice.

analysis and/or numerical engine. The Analysis engine supports standard model checking algorithms for CTL-style until-formulas, as well as graph algorithms, for instance to compute the bottom strongly connected components of a Markov chain. The former algorithms are used in a pre-processing phase during the checking of probabilistic until-formulas while the latter is needed when calculating steady state properties. The Numerical engine provides several methods for the numerical analysis of the CTMC such as linear solvers, methods for numerical integration and uniformisation. These are used to solve sytems of linear or integral equations. The State space manager represents the model in sparse matrix format. It maintains information about the validity of atomic propositions and of sub-formulas for each state. Status and Availability ETMCC has been used successfully in several non-trivial case studies, e.g. a cyclic server polling system and a multiprocessor mainframe with software failures. Its efficient numerical analysis methods enable users to check performability properties for models of up to several millions of states. The tool is available free of charge for academia, see http://www7.informatik.uni-erlangen.de/etmcc/ ,t he current download being version 1.4. A detailed description of ETMCC can be found in [4].

A method for analyzing the functional behavior and the performance of programs in distributed systems is presented. We use hybrid monitoring, a technique which combines advantages of both software monitoring and hardware monitoring. The paper contains a description of a hardware monitor and a software package (ZM4/SIMPLE) which make our concepts available to programmers, assisting them in debugging and tuning of their code. A short survey of related monitor systems highlights the distinguishing features of our implementation. As an application of our monitoring and evaluation system, the analysis of a parallel ray tracing program running on the SUPRENUM multiprocessor is described. It is shown that monitoring and modeling both rely on a common abstraction of a system's dynamic behavior and therefore can be integrated to one comprehensive methodology. This methodology is supported by a set of tools.>

It is often very difficult for programmers of parallel computers to understand how their parallel programs behave at execution time, because there is not enough insight into the interactions between concurrent activities in the parallel machine. Programmers do not only wish to obtain statistical information that can be supplied by profiling, for example. They need to have detailed knowledge about the functional behaviour of their programs. Considering performance aspects, they need timing information as well. Monitoring is a technique well suited to obtain information about both functional behaviour and timing. Global time information is essential for determining the chronological order of events on different nodes of a multiprocessor or of a distributed system, and for determining the duration of time intervals between events from different nodes. A major problem on multiprocessors is the absence of a global clock with high resolution. This problem can be overcome if a monitor system capable of supplying globally valid time stamps is used.