Gianfranco Ciardo's Publications

Publications are listed in reverse chronological order (most recent first) within the following categories:

• Journal papers
• Conference papers
• Book chapters
• Miscellanea

For most, an abstract is provided. For some, an online version can be retrieved.

Important Copyright Notice:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without explicit permission of the copyright holder.

R. Siminiceanu and G. Ciardo. Formal verification of the NASA Runway Safety Monitor. Software Tools for Technology Transfer, 9(1):63-76, 2007.

The Runway Safety Monitor (RSM) designed by Lockheed Martin is part of NASA's effort to reduce aviation accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool SMART to investigate a number of safety properties for the RSM. To mitigate the impact of state-space explosion, we built a highly discretized model of the system, obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the conceptual design of RSM. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with similar NuSMV and SPIN models have failed due to excessive memory consumption.

G. Ciardo, G. Luettgen, and A. S. Miner. Exploiting interleaving semantics in symbolic state-space generation. Formal Methods in System Design, 31:63-100, 2007.

Symbolic techniques based on Binary Decision Diagrams (BDDs) are widely employed for reasoning about temporal properties of hardware circuits and synchronous controllers. However, they often perform poorly when dealing with the huge state spaces underlying systems based on interleaving semantics, such as communications protocols and distributed software, which are composed of independently acting subsystems that communicate via shared events. This article shows that the efficiency of state-space exploration techniques using decision diagrams can be drastically improved by exploiting the interleaving semantics underlying many event-based and component-based system models. A new algorithm for symbolically generating state spaces is presented that (i) encodes a model's state vectors with Multi-valued Decision Diagrams (MDDs) rather than flattening them into BDDs and (ii) partitions the model's Kronecker-consistent next-state function by event and subsystem, thus enabling multiple lightweight next-state transformations rather than a single heavyweight one. Together, this paves the way for a novel iteration order, called saturation, which replaces the breadth-first search order of traditional algorithms. The resulting saturation algorithm is implemented in the tool SMART, and experimental studies show that it is often several orders of magnitude better in terms of time efficiency, final memory consumption, and peak memory consumption than existing symbolic algorithms.

G. Ciardo, R. Marmorstein, and R. Siminiceanu. The saturation algorithm for symbolic state space exploration. Software Tools for Technology Transfer, 8(1):4-25, 2006.

We present various algorithms for generating the state space of an asynchronous system, based on the use of multi-way decision diagrams to encode sets and Kronecker operators on boolean matrices to encode the next-state function. The Kronecker encoding allows us to recognize and exploit the ``locality of effect'' that events might have on state variables. In turn, locality information suggests better iteration strategies aimed at minimizing peak memory consumption. In particular, we focus on the saturation strategy, which is completely different from traditional breadth-first symbolic approaches, and extend its applicability to models where the possible values of the state variables are not known a priori. The resulting algorithm merges ``on-the-fly'' explicit state-space generation of each submodel with symbolic state-space generation of the overall model. Each algorithm we present is implemented in our tool SMART. This allows us to run fair and detailed comparisons between them, on a suite of representative models. Saturation, in particular, is shown to be many orders of magnitude more efficient in terms of memory and time with respect to traditional methods.

G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. Logical and stochastic modeling with SMART Performance Evaluation, 63:578-608, 2006.

We describe the main features of SMART, a software package providing a seamless environment for the logic and probabilistic analysis of complex systems. SMART can combine different formalisms in the same modeling study. For the analysis of logical behavior, both explicit and symbolic state-space generation techniques, as well as symbolic CTL model-checking algorithms, are available. For the study of stochastic and timing behavior, both sparse-storage and Kronecker numerical solution approaches are available when the underlying process is a Markov chain. In addition, discrete-event simulation is always applicable regardless of the stochastic nature of the process, but certain classes of non-Markov models can still be solved numerically. Finally, since SMART targets both the classroom and realistic industrial settings as a learning, research, and application tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.

G. Ciardo and A. Miner. Implicit data structures for logic and stochastic systems analysis. Performance Evaluation Review, 32(4):4-9, 2005.

Both logic and stochastic analysis have strong theoretical underpinnings, but they have been traditionally relegated to separate areas of computer science, the former focusing on logic and discrete algorithms, the latter on exact or approximate numerical methods. In the last few years, though, there has been a convergence of research in these two areas, due to the realization that data structures used in one area can benefit the other and that, by merging the goals of the two areas, a more integrated approach to system analysis can be derived. In this paper, we describe some of the beneficial interactions between the two, and some of the research challenges ahead.

Q. Zhang, A. Riska, W. Sun, E. Smirni, and G. Ciardo. Workload-aware load balancing for clustered web servers. IEEE Trans. Par. and Distr. Syst., 16(3):219-233. Mar. 2005.

We focus on load balancing policies for homogeneous clustered web servers that tune their parameters on-the-fly to adapt to changes in the arrival rates and service times of incoming requests. The proposed scheduling policy, AdaptLoad, monitors the incoming workload and self-adjusts its balancing parameters according to changes in the operational environment such as rapid fluctuations in the arrival rates or document popularity. Using actual traces from the 1998 World Cup web site, we conduct a detailed characterization of the workload demands and demonstrate how on-line workload monitoring can play a significant part in meeting the performance challenges of robust policy design. We show that the proposed load balancing policy based on statistical information derived from recent workload history provides similar performance benefits as locality-aware allocation schemes, without requiring locality data. Extensive experimentation indicates that AdaptLoad results in an effective scheme, even when servers must support both static and dynamic web pages.

G. Ciardo, A. Riska, and E. Smirni. ETAQA-MG1: An efficient technique for the analysis of M/G/1-type processes by aggregation. Performance Evaluation, 57(3):235-260. July 2004.

We extend the ETAQA approach, initially proposed for the efficient numerical solution of a class of quasi birth-death processes, to a more complex class of M/G/1-type Markov processes where arbitrary forward transitions are allowed but backward transitions must be to a single state to the previous level. The new technique reduces the exact solution of this class of M/G/1-type models to that of a finite linear system. We demonstrate the utility of our method by describing the exact computation of an extensive class of Markov reward functions that include the expected queue length or its higher moments. We also provide an algorithm that finds an appropriate state reordering satisfying our applicability conditions, if one such order exists. We illustrate the method, discuss its complexity and numerical stability, and present comparisons with other traditional techniques.

A. Riska, E. Smirni, and G. Ciardo. Exact analysis of a class of GI/G/1-type performability models. IEEE Trans. Rel., 53(2):238-249, June 2004.

We present an exact decomposition algorithm for the analysis of Markov chains with a GI/G/1-type repetitive structure. Such processes exhibit both M/G/1-type and GI/M/1-type patterns, and cannot be solved using existing techniques. Markov chains with a GI/G/1 pattern result when modeling open systems which accept jobs from multiple exogenous sources, and are subject to failures and repairs; a single failure can empty the system of jobs, while a single batch arrival can add many jobs to the system. Our method provides exact computation of the stationary probabilities, which can then be used to obtain performance measures such as the average queue length or any of its higher moments, as well as the probability of the system being in various failure states, thus performability measures. We formulate the conditions under which our approach is applicable, and illustrate it via the performability analysis of a parallel computer system.

A. Riska, E. Smirni, and G. Ciardo. An aggregation-based method for the exact analysis of a class of GI/G/1-type processes. Performance Evaluation Review, 31(2):28-30, Sept. 2003.

We present an aggregation-based algorithm for the exact analysis of Markov chains with GI/G/1-type pattern in their repetitive structure, i.e., chains that exhibit both M/G/1-type and GI/M/1-type patterns and cannot be solved with existing techniques. Markov chains with a GI/G/1 pattern result when modeling open systems with faults/repairs that accept jobs from multiple exogenous sources. Our method provides exact computation of the steady state probabilities, and consequently allows computation of performance measures of interest including the system queue length or any of its higher moments, the exact probability of system failures and repairs, and consequently a host of performability measures. Our algorithm can also apply to systems that are purely of the M/G/1-type or the GI/M/1-type, or their intersection, i.e., quasi-birth-death processes.

G. Ciardo, A. Riska, and E. Smirni. EQUILOAD: a load balancing policy for clustered web servers. Performance Evaluation, 46(2-3):102:124, 2001.

We present a new strategy for the allocation of requests in clustered web servers, based on the size distribution of the requested documents. This strategy, EQUILOAD, manages to achieve a balanced load to each of the back-end servers, and its parameters are obtained from the analysis of a trace's past data. To study its performance, we use phase-type distribution fittings and solve the resulting models using a new solution method for M/PH/1 queues that only requires solution of linear systems. The results show that EQUILOAD greatly outperforms random allocation, performs comparably or better than the Shortest Remaining Processing Time and Join Shortest Queue policies and maximizes cache hits at the back-end servers, therefore behaving similarly to a ``locality-aware'' allocation policy, but at a very low implementation cost.

P. Buchholz, G. Ciardo, P. Kemper, and S. Donatelli. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS Journal on Computing, 13(3):203:222, 2000.

We present new algorithms for the solution of large structured Markov models whose infinitesimal generator can be expressed as a Kronecker expression of sparse matrices. We then compare them with the shuffle-based method commonly used in this context and show how our new algorithms can be advantageous in dealing with very sparse matrices and in supporting both Jacobi-style and Gauss-Seidel-style methods with appropriate multiplication algorithms. Our main contribution is to show how solution algorithms based on Kronecker expression can be modified to consider probability vectors of size equal to the ``actual'' state space instead of the ``potential'' state space, thus providing space and time savings. The complexity of our algorithms is compared under different sparsity assumptions. A nontrivial example is studied to illustrate the complexity of the implemented algorithms.

G. Ciardo and E. Smirni. ETAQA: An Efficient Technique for the Analysis of QBD-processes by Aggregation Perf. Eval., 36-37:71-93, 1999.

In this paper we present ETAQA, an Efficient Technique for the Analysis of QBD-processes by Aggregation. We concentrate on processes satisfying a particular repetitive structure that frequently occurs in modeling of computer and communication systems. The proposed methodology exploits this special structure to evaluate the aggregate probability distribution of the states in each of the equivalence classes corresponding to a specific partitioning of the state space. Although the method does not compute the probability distribution of all states in the chain, not even in implicit recursive form, it provides the necessary information to easily compute an extensive set of Markov reward functions such as the queue length or any of its higher moments. The proposed technique has excellent computational and storage complexity and results in significant savings when compared with other traditional solution techniques such as the matrix geometric approach.},

G. Ciardo, D. Nicol, K. Trivedi. Discrete-event simulation of fluid stochastic Petri nets. IEEE Trans. Softw. Eng., 25(2):207-217, March/April 1999.

The purpose of this paper is to describe a method for the simulation of the recently introduced fluid stochastic Petri nets. Since such nets result in rather complex system of partial differential equations, numerical solution becomes a formidable task. Because of a mixed (discrete and continuous) state space, simulative solution also poses some interesting challenges, which are addressed in the paper.

G. Ciardo and G. Li. Approximate transient analysis for subclasses of deterministic and stochastic Petri nets. Perf. Eval., 35:109-129, 1999.

Transient analysis of non-Markovian Stochastic Petri nets is a theoretically interesting and practically important problem. In this paper, we first present a method to compute bounds and an approximation on the average state sojourn times for a subclass of deterministic and stochastic Petri nets (DSPNs) where there is a single persistent deterministic transition that can become enabled only in a special state. Then, we extend this class by allowing the transition to become enabled in any state, as long as the time between successive enablings of the deterministic transition is independent of this state, and develop a new approximate transient analysis approach. In addition to renewal theory, we only make use of discrete and continuous Markov chain concepts. As an application, we use the model of a finite-capacity queue with a server subject to breakdowns, and assess the quality of our approximations.

G. Ciardo, J. Gluckman, and D. Nicol. Distributed state-space generation of discrete-state stochastic models. INFORMS J. Comp., 10(1):82--93, 1998.

High-level formalisms such as stochastic Petri nets can be used to model complex systems. Analysis of logical and numerical properties of these models often requires the generation and storage of the entire underlying state space. This imposes practical limitations on the types of systems which can be modeled. Because of the vast amount of memory consumed, we investigate distributed algorithms for the generation of state space graphs. The distributed construction allows us to take advantage of the combined memory readily available on a network of workstations. The key technical problem is to find effective methods for on-the-fly partitioning, so that the state space is evenly distributed among processors. In this paper we report on the implementation of a distributed state space generator that may be linked to a number of existing system modeling tools. We discuss partitioning strategies in the context of Petri net models, and report on performance observed on a network of workstations, as well as on a distributed memory multi-computer.

D. Nicol and G. Ciardo. Automated parallelization of discrete state-space generation. Journal of Parallel and Distributed Computing, 47:153-167, 1997.

We consider the problem of generating a large state-space in a distributed fashion. Unlike previously proposed solutions that partition the set of reachable states according to a hashing function provided by the user, we explore heuristic methods that completely automate the process. The first step is an initial random walk through the state space to initialize a search tree, duplicated in each processor. Then, the reachability graph is built in a distributed way, using the search tree to assign each newly found state to classes assigned to the available processors. Furthermore, we explore two remapping criteria that attempt to balance memory usage or future workload, respectively. We show how the cost of computing the global snapshot required for remapping will scale up for system sizes in the foreseeable future. An extensive set of results is presented to support our conclusions that remapping is extremely beneficial.

G. Ciardo, L. M. Leemis, and D. Nicol. On the minimum of independent geometrically distributed random variables. Statistics and probability letters, 23:313-326, 1995.

The expectations E[X], E[Z], and E[Y] of the minimum of n independent geometric, modified geometric, or exponential random variables with matching expectations differ. We show how this is accounted for by stochastic variability and how E[X]/E[Y] equals the expected number of ties at the minimum for the geometric random variables. We then introduce the ``shifted geometric distribution'', and show that there is a unique value of the shift for which the individual shifted geometric and exponential random variables match expectations both individually and in their minimums.

G. Ciardo and C. Lindemann. Comments on ``Analysis of self-stabilizing clock synchronization by means of stochastic Petri nets''. IEEE Trans. Comp., 43(12):1453-1456, Dec. 1994.

We correct some problems in the approach presented by Lu, Zhang, and Murata in their paper ``Analysis of self-stabilizing clock synchronization by means of stochastic Petri nets'', then we study the same system using the computer package DSPNexpress, and present the computational effort as a function of the number of clocks in the system.

J. K. Muppala, G. Ciardo, and K. S. Trivedi. Stochastic reward nets for reliability prediction. Communications in Reliability, Maintenability and Serviceability, 1(2):9-20, July 1994.

We describe the use of stochastic Petri nets (SPNs) and stochastic reward nets (SRNs) which are SPNs augmented with the ability to specify output measures as reward-based functions, for the evaluation of reliability for complex systems. The solution of SRNs involves generation and analysis of the corresponding Markov reward model. The use of SRNs in modeling complex systems is illustrated through several interesting examples. We mention the use of the Stochastic Petri Net Package (SPNP) for the description and solution of SRN models.

G. Ciardo, R. German, and C. Lindemann. A characterization of the stochastic process underlying a stochastic Petri net. IEEE Trans. Softw. Eng., 20(7):506-515, July 1994.

Stochastic Petri nets (SPNs) with generally distributed firing times can model a large class of systems, but simulation is the only feasible approach for their solution. We explore a hierarchy of SPN classes where modeling power is reduced in exchange for an increasingly efficient solution. Generalized stochastic Petri nets (GSPNs), deterministic and stochastic Petri nets (DSPNs), semi-Markovian stochastic Petri nets (SM-SPNs), timed Petri nets (TPNs), and generalized timed Petri nets (GTPNs) are particular entries in our hierarchy. Additional classes of SPNs for which we show how to compute an analytical solution are obtained by the method of the embedded Markov chain (DSPNs are just one example in this class) and state discretization, which we apply not only to the continuous-time case (PH-type distributions), but also to the discrete case.

G. Ciardo and K. S. Trivedi. A decomposition approach for stochastic reward net models. Perf. Eval., 18(1):37-59, 1993.

We present a decomposition approach for the solution of large stochastic reward nets (SRNs) based on the concept of near-independence. The overall model consists of a set of submodels whose interactions are described by an import graph. Each node of the graph corresponds to a parametric SRN submodel and an arc from submodel A to submodel B corresponds to a parameter value that B must receive from A. The quantities exchanged between submodels are based on only three primitives. The import graph normally contains cycles, so the solution method is based on fixed point iteration. Any SRN containing one or more of the nearly-independent structures we present, commonly encountered in practice, can be analyzed using our approach. No other restriction on the SRN is required. We apply our technique to the analysis of a flexible manufacturing system.

G. Ciardo, J. K. Muppala, and K. S. Trivedi. Analyzing concurrent and fault-tolerant software using stochastic Petri nets. J. Par. and Distr. Comp., 15(3):255-269, July 1992.

We present two software applications and develop models for them. The first application considers a producer-consumer tasking system with an intermediate buffer task and studies how the performance is affected by different selection policies when multiple tasks are ready to synchronize. The second application studies the reliability of a fault-tolerant software system using the recovery block scheme. The model is incrementally augmented by considering clustered failures or the effective arrival rate of inputs to the system. We use stochastic reward nets, a variant of stochastic Petri nets, to model the two software applications. In both models, each quantity to be computed is defined in terms of either the expected value of a reward rate in steady-state or at a given time theta, or as the expected value of the accumulated reward until absorption or until a given time theta. This allows extreme flexibility while maintaning a rigorous formalization of these quantities.

G. Ciardo, J. K. Muppala, and K. S. Trivedi. On the solution of GSPN reward models. Perf. Eval., 12(4):237-253, 1991.

We extend the basic GSPN (generalized stochastic Petri net) model to GSPN-reward model. This allows the concise specification of both the underlying stochastic process and the rewards attached to the states and the transitions of the stochastic process. The classical method for the steady-state solution of GSPN models, based on the correspondence between GSPNs and continuous-time Markov chains (CTMCs), is compared with a method based on discrete-time Markov chains (DTMCs) previously judged poor. We show that there are GSPNs when the DTMC-based method performs better than the classical method (and others where it performs worse). Finally, we discuss how to perform parametric sensitivity analysis on the measures computed from a GSPN using either solution method.

G. Ciardo, R. A. Marie, B. Sericola, and K. S. Trivedi. Performability analysis using semi-Markov reward processes. IEEE Trans. Comp., 39(10):1251-1264, Oct. 1990.

With the increasing complexity of multiprocessor and distributed processing systems, the need to develop efficient and accurate modeling methods is evident. Fault-tolerance and degradable performance of such systems has given rise to considerable interest in models for the combined evaluation of performance and reliability. Most of these models are based upon Markov or semi-Markov reward processes. Beaudry proposed a simple method for computing the distribution of performability in a Markov reward process. We present two extensions of Beaudry's approach. First, we generalize the method to a semi-Markov reward process. Second, we remove the restriction requiring the association of zero reward to absorbing states only. Such reward models can be used to evaluate the effectiveness of degradable fault-tolerant systems. We illustrate the use of the approach with three interesting applications.

A. L. Reibman, K. S. Trivedi, S. Kumar, and G. Ciardo. Analysis of stiff Markov chains. ORSA J. Comp., 1(2), Spring 1989.

Continuous-time Markov chains (CTMCs) are widely used mathematical models. Reliability models, queueing networks, and inventory models all require transient solution of CTMCs. The cost of CTMC transient solution increases with size, stiffness, and mission time. To eliminate stiffness and reduce the cost of solution, approximation techniques have been proposed. In this paper, we describe a software package for the specification and solution of stiff CTMC. As an interface, we use a language for the description of Markov chains. The language also provides facilities for controlling the solution procedure. Both exact and approximate solution techniques are provided. To conclude the paper, we use several examples to show the use of our specification language and the utility of our approximation technique.

J. Bechta Dugan and G. Ciardo. Stochastic Petri net analysis of a replicated file system. IEEE Trans. Softw. Eng., 15(4):394-401, Apr. 1989.

We present a stochastic Petri net model of a replicated file system in a distributed environment where replicated files reside on different hosts and a voting algorithm is used to maintain consistency. Witnesses, which simply record the status of the file but contain no data, may be used in addition to or in place of files to reduce overhead. We present a model sufficiently detailed to include file status (current or out-of-date) as well as failure and repair of hosts where copies or witnesses reside. The number of copies and witnesses is not fixed, but is a parameter of the model. Two different majority protocols are examined, one where a majority of all copies and witnesses is necessary to form a quorum, the other where only a majority of the copies and witnesses on operational hosts is needed. The latter, known as adaptive voting, is shown to increase file availability in most cases. We also investigate the process of selection of copies and witnesses to participate in an update when more than the majority is available and show the inherent performance/reliability tradeoffs.

A. J. Yu, G. Ciardo, and G. Luettgen. Bounded reachability checking of asynchronous systems using decision diagrams. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 648-663. Braga, Portugal, March 2007.

Bounded reachability or model checking is widely believed to work poorly when using decision diagrams instead of SAT procedures. Recent research suggests this to be untrue with regards to synchronous systems, particularly digital circuits. This paper shows that the belief is also a myth for asynchronous systems, such as models specified by Petri nets. We propose Bounded Saturation, a new algorithm to compute bounded state spaces using Multi-way Decision Diagrams (MDDs). This is based on the established Saturation algorithm which benefits from a non-standard search strategy that is very different from breadth-first search. To bound Saturation, we employ Edge-Valued MDDs and rework its search strategy. Experimental results show that our algorithm often, but not always, compares favorably against two SAT-based approaches advocated in the literature for deadlock checking in Petri nets.

M.-Y. Chung, G. Ciardo, and R. Siminiceanu. Caching, hashing, and garbage collection for distributed state space construction. In Proc. Workshop on Parallel and Distributed Model Checking (PDMC), pages 121-136. Berlin, Germany, July 2007.

The Saturation algorithm for symbolic state-space generation is a recent advance in exhaustive verification of complex systems, in particular globally-asynchronous/ locally-synchronous systems. The distributed version of Saturation uses the overall memory available on a network of workstations (NOW) to efficiently spread the memory load during its highly irregular exploration. A crucial factor in limiting the memory consumption in symbolic state-space generation is the ability to perform garbage collection to free up the memory occupied by dead nodes. However, garbage collection over a NOW requires a nontrivial communication overhead. In addition, operation cache policies become critical while analyzing large-scale systems using a symbolic approach. In this paper, we develop a garbage collection scheme and several operation cache policies to help the analysis of complex systems. Experiments show that our schemes improve the performance of the original distributed implementation, SmartNOW, in terms of both time and memory efficiency.

J. Ezekiel, G. Luettgen, and G. Ciardo. Parallelising symbolic state-space generators. In Proc. Computer Aided Verification (CAV), pages 268-280. Berlin, Germany, July 2007.

Symbolic state-space generators are notoriously hard to parallelise, largely due to the irregular nature of the task. Parallel languages such as Cilk, tailored to irregular problems, have been shown to offer efficient scheduling and load balancing. This paper explores whether Cilk can be used to efficiently parallelise a symbolic state-space generator on a shared-memory architecture. We parallelise the Saturation algorithm implemented in the SMART verification tool using Cilk, and compare it to a parallel implementation of the algorithm using a thread pool. Our experimental studies on a dual-processor, dual-core PC show that Cilk can improve the run-time efficiency of our parallel algorithm due to its load balancing and scheduling efficiency. We also demonstrate that this incurs a significant memory overhead due to Cilk's inability to support pipelining, and conclude by pointing to a possible future direction for parallel irregular languages to include pipelining.

G. Ciardo, G. Luettgen, and A. J. Yu. Improving static variable orders via invariants. In Proc. 28th International Conference on Application and Theory of Petri nets and Other Models of Concurrency (ICATPN), pages 83-103. Siedlce, Poland, June 2007.

Choosing a good variable order is crucial for making symbolic state-space generation algorithms truly efficient. One such algorithm is the MDD-based Saturation algorithm for Petri nets implemented in SMART, whose efficiency relies on exploiting event locality. This paper presents a novel, static ordering heuristic that considers place invariants of Petri nets. In contrast to related work, we use the functional dependencies encoded by invariants to merge decision-diagram variables, rather than to eliminate them. We prove that merging variables always yields smaller MDDs and improves event locality, while eliminating variables may increase MDD sizes and break locality. Combining this idea of merging with heuristics for maximizing event locality, we obtain an algorithm for static variable order which outperforms competing approaches regarding both time-efficiency and memory-efficiency, as we demonstrate by extensive benchmarking.

M.-Y. Chung, G. Ciardo, and A. J. Yu. A fine-grained fullness-guided chaining heuristic for symbolic reachability analysis. In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), pages 51-66. Beijing, China, Oct. 2006.

Chaining can reduce the number of iterations required for symbolic state-space generation and model-checking, especially in Petri nets and similar asynchronous systems, but requires considerable insight and is limited to a static ordering of the events in the high-level model. We introduce a two-step approach that is instead fine-grained and dynamically applied to the decision diagrams nodes. The first step, based on a precedence relation, is guaranteed to improve convergence, while the second one, based on a notion of node fullness, is heuristic. We apply our approach to traditional breadth-first and saturation state-space generation, and show that it is effective in both cases.

R. Siminiceanu and G. Ciardo. New metrics for static variable ordering in decision diagrams. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 90-104. Vienna, Austria, March 2006.

We investigate a new class of metrics to find good variable orders for decision diagrams in symbolic state-space generation. Most of the previous work on static ordering is centered around the concept of minimum variable span, which can also be found in the literature under several other names. We use a similar concept, but applied to event span, and generalize it to a family of metrics parameterized by a moment, where the metric of moment 0 is the combined event span. Finding a good variable order is then reduced to optimizing one of these metrics, and we design extensive experiments to evaluate them. First, we investigate how the actual optimal order performs in state-space generation, when it can be computed by evaluating all possible permutations. Then, we study the performance of these metrics on selected models and compare their impact on two different state-space generation algorithms: classic breadth-first and our own saturation strategy. We conclude that the new metric of moment 1 is the best choice. In particular, the saturation algorithm seems to benefit the most from using it, as it achieves the better performance in nearly 80% of the cases.

M.-Y. Chung and G. Ciardo. A dynamic firing speculation to speedup distributed symbolic state-space generation. In Proc. International Parallel and Distributed Processing Symposium (IPDPS), Rodos, Greece, April 2006.

The saturation strategy for symbolic state-space generation is very effective for globally-asynchronous locally-synchronous discrete-state systems. Its inherently sequential nature, however, makes it difficult to parallelize on a NOW. An initial attempt that utilizes idle workstations to recognize event firing patterns and then speculatively compute firings conforming to these patterns is at times effective but can introduce large memory overheads. We suggest an implicit method to encode the firing history of decision diagram nodes, where patterns can be shared by nodes. By preserving the actual firing history efficiently and effectively, the speculation is more informed. Experiments show that our implicit encoding method not only reduces the memory requirements but also enables dynamic speculation schemes that further improve runtime.

G. Ciardo and A. J. Yu. Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In Proc. Correct Hardware Design and Verification Methods (CHARME) , pages 146-161. Saarbrucken, Germany, Oct. 2005.

We propose a new saturation-based symbolic state-space generation algorithm for finite discrete-state systems. Based on the structure of the high-level model specification, we first disjunctively partition the transition relation of the system, then conjunctively partition each disjunct. Our new encoding recognizes identity transformations of state variables and exploits event locality, enabling us to apply a recursive fixed-point image computation strategy completely different from the standard breadth-first approach employing a global fix-point image computation. Compared to breadth-first symbolic methods, saturation has already been empirically shown to be several orders more efficient in terms of runtime and peak memory requirements for asynchronous concurrent systems. With the new partitioning, the saturation algorithm can now be applied to completely general asynchronous systems, while requiring similar or better run-times and peak memory than previous saturation algorithms.

G. Ciardo. Implicit representations and algorithms for the logic and stochastic analysis of discrete--state systems In Proc. Formal Techniques for Computer Systems and Business Processes , pages 15-17. Paris, France, Sept. 2005.

(Invited Keynote Paper)

M.-Y. Chung and G. Ciardo. A pattern recognition approach for speculative firing prediction in distributed saturation state-space generation. In Proc. Workshop on Parallel and Distributed Model Checking (PDMC) , pages 65-79. Lisbon, Portugal, July 2005.

The saturation strategy for symbolic state-space generation is particularly effective for globally-asynchronous locally-synchronous systems. A distributed version of saturation, SaturationNOW, uses the overall memory available on a network of workstations to effectively spread the memory load, but its execution is essentially sequential. To achieve true parallelism, we explore a speculative firing prediction, where idle workstations work on predicted future event firing requests. A naive approach where all possible firings may be explored a priori, given enough idle time, can result in excessive memory requirements. Thus, we introduce a history-based approach for firing prediction that recognizes firing patterns and explores only firings conforming to these patterns. Experiments show that our heuristic improves the runtime and has a small memory overhead.

R. Siminiceanu and G. Ciardo. Formal verification of the NASA runway safety monitor. In Electronic Notes in Theoretical Computer Science, Proc. Fourth International Workshop on Automated Verification of Critical Systems (AVoCS'04), London, UK, Sept. 2004.

The Runway Safety Monitor (RSM) designed by Lockheed Martin is part of NASA's effort to reduce aviation accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool SMART to investigate behaviors that can be classified as missed alarm scenarios in RSM. To apply discrete-state techniques and mitigate the impact of the resulting state-space explosion phenomenon, our model uses a highly discretized view of the system obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the RSM conceptual design. Our findings were forwarded to the design engineers, who undertook corrective action. The results stress the high level of efficiency attained by the new model checking algorithms implemented in our tool SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with NuSMV and SPIN have failed due to excessive memory consumption.

M.-Y. Chung, G. Ciardo. Saturation NOW In Proc. QEST, pages 272-281. Enschede, The Netherlands, Sept. 2004.

We present a distributed version of the saturation algorithm for symbolic state-space generation of discrete-state models. The execution is strictly sequential but utilizes the overall available memory. Thanks to a level-based allocation of the decision diagram nodes onto the workstations, no additional node or work is created. A dynamic memory load balancing heuristic helps coping with the uneven growth of the decision diagram levels allocated to each workstation. Experiments on a conventional network of workstations show that the runtime of our distributed implementation is close to the sequential one even when balancing is triggered, while it is of course much better when the sequential implementation is forced to rely on virtual memory.

G. Ciardo. Reachability set generation for Petri nets: can brute force be smart? (Invited Talk). In Proc. 25th Int. Conf. on Applications and Theory of Petri Nets, pages 17-34. Bologna, Italy, June 2004.

We present a new technique for the generation and storage of the reachability set of a Petri net. Our approach is inspired by previous work on Binary and Multi-valued Decision Diagrams but exploits a concept of locality for the effect of a transition's firing to vastly improve algorithmic performance. The result is a data structure and a set of manipulation routines that can be used to generate and store enormous sets extremely efficiently in terms of both memory and execution time.

Q. Zhang, E. Smirni, and G. Ciardo. Profit-driven service differentiation in transient environments. In Proc. 11th IEEE/ACM Int. Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), pages 230-233. Orlando, FL, USA, Oct. 2003.

We focus on service differentiation policies for Web servers where clients have different QoS requirements and the environment has large fluctuations in the client arrival and service patterns and in the QoS class mix. We propose an adaptive admission control mechanism that offers service differentiation among client classes and maximizes the effectiveness of the server's operation. Using actual traces from the 1998 World Cup web site, we conduct a detailed analysis of the proposed policy and show that it meets the performance challenges of a robust QoS policy.

G. Ciardo and Y. Lan. Faster discrete-event simulation through structural caching. In Proc. Sixth Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-6), pages 11-14. Urbana, IL, USA, Sept. 2003.

We develop a structural caching strategy to improve the performance of simulation for a wide class of models expressed in high-level formalisms. By imposing a Kronecker consistent partition of a model into submodels, we compute once, and cache for future use, the effect of each event on each submodel. This greatly reduces the cost of processing events, updating the current state, and collecting statistics.

R. Jones and G. Ciardo. Regenerative simulation of stochastic Petri nets with discrete and continuous timing. In Proc. Sixth Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-6), pages 23-26. Urbana, IL, USA, Sept. 2003.

We present a regenerative simulation method applicable to a special class of non-Markovian stochastic Petri net (SPN) that may be useful in practice for constructing and solving performability models. Introduced in [Jones and Ciardo 2001], this special SPN is called a phased delay Petri net (PDPN) and was conceived to allow efficient numerical analysis while increasing the modeling fidelity. The PDPN permits phase-type firing delays in both discrete and continuous time simultaneously in the same model. However, exact numerical analysis requires that the discrete-time transitions be synchronized when active. We propose here, instead, a new regenerative simulation technique that offers efficient analysis of PDPNs where numerical solution by exact means or other (known) types of regenerative simulation is too difficult.

G. Ciardo, M. Forno, P. Grieco, and A. Miner. Comparing implicit representations of large CTMCs. In Numerical Solution of Markov Chains, pages 323-327. Urbana, IL, USA, Sept. 2003.

High-level formalisms of stochastic structures can express very large continuous-time Markov chains (CTMC). State explosion poses interesting challenges in terms of data structures and numerical solution algorithms. Implicit representations exploit structural properties of the high-level model, to avoid storing each nonzero matrix entry explicitly. Implicit structures used to store the CTMC include Kronecker algebra, multi-terminal BDDs, and matrix diagrams, all of which require specialized multiplication algorithms. These methods can be very compact in practice, although in the worst case they require more memory than explicit storage. In this paper, we begin an in-depth comparison of implicit CTMC techniques, we present some initial observations and discuss the currently-known tradeoffs between the various techniques. We identify several questions that are worth further investigation.

G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. Logical and stochastic modeling with SMART. In Proc. Tools 2003, LNCS 2794, pages 78-97. Urbana-Champaign, IL, USA, Sept. 2003. Springer-Verlag.

We describe the main features of SMART, a software package providing a seamless environment for the logic and probabilistic analysis of complex systems. SMART can combine different formalisms in the same modeling study. For the analysis of logical behavior, both explicit and symbolic state-space generation techniques, as well as symbolic CTL model-checking algorithms, are available. For the study of stochastic and timing behavior, both sparse-storage and Kronecker numerical solution approaches are available when the underlying process is a Markov chain. In addition, discrete-event simulation is always applicable regardless of the stochastic nature of the process, but certain classes of non-Markov models can still be solved numerically. Finally, since SMART targets both the classroom and realistic industrial settings as a learning, research, and application tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.

G. Ciardo and R. Siminiceanu. Structural symbolic CTL model checking of asynchronous systems. In Proc. Computer Aided Verification (CAV 2003), LNCS 2725, pages 40-53. Boulder, CO, USA, July 2003. Springer-Verlag.

In previous work, we showed how structural information can be used to efficiently generate the state-space of asynchronous systems. Here, we apply these ideas to symbolic CTL model checking. Thanks to a Kronecker encoding of the transition relation, we detect and exploit event locality and apply better fixed-point iteration strategies, resulting in orders-of-magnitude reductions for both execution times and memory consumption in comparison to well-established tools such as NuSMV.

G. Ciardo, R. Marmorstein, and R. Siminiceanu. Saturation unbound. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), LNCS 2619, pages 379-393. Warsaw, Poland, Apr. 2003. Springer-Verlag.

In previous work, we proposed a ``saturation'' algorithm for symbolic state-space generation characterized by the use of multi-valued decision diagrams, boolean Kronecker operators, event locality, and a special iteration strategy. This approach outperforms traditional BDD-based techniques by several orders of magnitude in both space and time but, like them, assumes a priori knowledge of each submodel's state space. We introduce a new algorithm that merges explicit local state-space discovery with symbolic global state-space generation. This relieves the modeler from worrying about the behavior of submodels in isolation.

G. Ciardo and R. Siminiceanu. Using edge-valued decision diagrams for symbolic generation of shortest paths. In Proceedings of the Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS 2517, pages 256-273. Portland, OR, USA, Nov. 2002. Springer-Verlag.

We present a new method for the symbolic construction of shortest paths in reachability graphs. Our algorithm relies on a variant of edge--valued decision diagrams that supports efficient fixed--point iterations for the joint computation of both the reachable states and their distance from the initial states. Once the distance function is known, a shortest path from an initial state to a state satisfying a given condition can be easily obtained. Using a few representative examples, we show how our algorithm is vastly superior, in terms of both memory and space, to alternative approaches that compute the same information, such as ordinary or algebraic decision diagrams.

A. Riska, W. Sun, E. Smirni, and G. Ciardo. AdaptLoad: effective balancing in clustered web servers under transient load conditions. In Proceedings of the 22nd International Conference on Distributed Computing Systems (ICDCS), pages 104-111. Vienna, Austria, July 2002. IEEE Computer Society Press.

We focus on adaptive policies for load balancing in clustered web servers, based on the size distribution of the requested documents. The proposed scheduling policy, AdaptLoad, adapts its balancing parameters on-the-fly, according to changes in the behavior of the customer population such as fluctuations in the intensity of arrivals or document popularity. Detailed performance comparisons via simulation using traces from the 1998 World Cup show that AdaptLoad is robust as it consistently outperforms traditional load balancing policies, especially under conditions of transient overload.

G. Ciardo. What a structural world (Keynote Talk). In Proc. 9th Int. Workshop on Petri Nets and Performance Models (PNPM'01) , pages 3-16. Aachen, Germany, Sept. 2001. IEEE Comp. Soc. Press.

Petri nets and stochastic Petri nets have been widely adopted as one of the best tools to model the logical and timing behavior of discrete-state systems. However, their practical applicability is limited by the state-space explosion problem. We survey some of the techniques that have been used to cope with large state spaces, starting from early explicit methods, which require data structures of size proportional to the number of states or state-to-state transitions, then moving to implicit methods, which borrow ideas from symbolic model checking (binary decision diagrams) and numerical linear algebra (Kronecker operators) to drastically reduce the computational requirements. Next, we describe the structural decomposition approach which has been the topic of our research in the last few years. This method only requires to specify a partition of the places in the net and, combining decision diagrams and Kronecker operators with the new concepts of event locality and node saturation, achieves fundamental gains in both memory and time efficiency. At the same, the approach is applicable to a wide range of models. We conclude by considering several research directions that could further push the range of solvable models, eventually leading to an even greater industrial acceptance of this simple yet powerful modeling formalism.

R. L. Jones and G. Ciardo. On phased delay stochastic Petri nets: Definition and an application. In Proc. 9th Int. Workshop on Petri Nets and Performance Models (PNPM'01) , pages 165-174. Aachen, Germany, Sept. 2001. IEEE Comp. Soc. Press.

We present a novel stochastic Petri net formalism where both discrete and continuous phase-type firing delays can appear simultaneously in the same model. By capturing non-Markovian behavior in discrete or continuous time, as appropriate, the formalism affords higher modeling fidelity. Alone, discrete or continuous phase-type Petri nets have simple underlying Markov chains, but mixing the two complicates matters. We show that, in a mixed model where discrete-time transitions are synchronized, the underlying process is semi-regenerative and we can employ Markov renewal theory to formulate stationary or time-dependent solutions. Also noteworthy are the computational trade-offs between the so-called embedded and subordinate Markov chains, which we employ to improve the overall solution efficiency. We present a preliminary stationary solution method that shows promise in terms of time and space efficiency and demonstrate it on an aeronautical data link system application.

L. Cherkasova and G. Ciardo. Role of aging, frequency, and size in Web cache replacement policies. In Proc. European Conference on High Performance Computing and Networking Europe (HPCN 2001), pages 114-123. Amsterdam, The Netherlands, June 2001.

Document caching on is used to improve Web performance. An efficient caching policy keeps popular documents in the cache and replaces rarely used ones. The latest web cache replacement policies incorporate the document size, frequency, and age in the decision process. The recently-proposed and very popular Greedy-Dual-Size (GDS) policy is based on document size and has an elegant aging mechanism. Similarly, the Greedy-Dual-Frequency (GDF) policy takes into account file frequency and exploits the aging mechanism to deal with cache pollution. The efficiency of a cache replacement policy can be evaluated along two popular metrics: file hit ratio and byte hit ratio. Using four different web server logs, we show that GDS-like replacement policies emphasizing size yield the best file hit ratio but typically show poor byte hit ratio, while GDF-like replacement policies emphasizing frequency have better byte hit ratio but result in worse file hit ratio. In this paper, we propose a generalization of Greedy-Dual-Frequency-Size policy which allows to balance the emphasis on size vs. frequency. We perform a sensitivity study to derive the impact of size and frequency on file and byte hit ratio, identifying parameters that aim at optimizing both metrics.

G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: an efficient iteration strategy for symbolic state-space generation. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), pages 328-342. Genova, Italy, Apr. 2001. Springer-Verlag.

We present a novel algorithm for generating state spaces of asynchronous systems using Multi-valued Decision Diagrams. In contrast to related work, we encode the next-state function of a system not as a single Boolean function, but as cross-products of integer functions. This permits the application of various iteration strategies to build a system's state space. In particular, we introduce a new elegant strategy, called saturation, and implement it in the tool SMART. On top of usually performing several orders of magnitude faster than existing BDD-based state-space generators, our algorithm's required peak memory is often close to the final memory needed for storing the overall state space.

L. Cherkasova and G. Ciardo. Characterizing temporal locality and its impact on Web server performance. In Proc. IEEE International Conference on Computer Communication and Networks (ICCCN 2000), pages 434-441. Las Vegas, NV, Oct. 2000. IEEE Comp. Soc. Press.

The presence of temporal locality in web traces has been long recognized. However, the close proximity of requests for the same file in a trace can be attributed to two orthogonal reasons: long-term popularity and short-term correlation. The former reflects the fact that requests for a popular document appear ``frequently'' thus they are likely to be ``close'' in an absolute sense. The latter reflects the fact that requests for a given document might concentrate around particular points in the trace due to a variety of reasons, such as deadlines or surges in user interests, hence it focuses on ``relative'' closeness. We introduce a new measure of temporal locality, the scaled stack distance, which is insensitive to popularity and captures instead the impact of short-term correlation, and use it to parametrize a synthetic trace generator. Then, we validate the appropriateness of this quantity by comparing the file and byte miss ratios corresponding to either the original or the synthetic traces.

A. Riska, E. Smirni, and G. Ciardo. Analytic modeling of load balancing policies for tasks with heavy-tailed distributions. In Proceedings of the Workshop on Software Performance Analysis (WOSP), pages 147-157. Ottawa, Canada, Sept. 2000. ACM Press.

We present an analytic technique for modeling load balancing policies on a cluster of servers conditioned on the fact that the service times of arriving tasks are drawn from heavy tail distributions. We propose a new modeling methodology for the exact solution of an M/H_k/1 server and illustrate its use for modeling two distinct load balancing policies in a distributed multi-server system. Our analytic results provide exact information regarding the distribution of task sizes that compose the waiting queue on each server and suggest an easy and inexpensive way to provide load balancing based on the sizes of the incoming tasks.

G. Ciardo, G. Luettgen, and Siminiceanu. Efficient symbolic state-space construction for asynchronous systems. In M. Nielsen and D. Simpson, editors, Application and Theory of Petri Nets 2000, Lecture Notes in Computer Science 1825, (Proceedings of the 21th International Conference on Applications and Theory of Petri Nets, Aarhus, Denmark), pages 103-122. June 2000. Springer-Verlag.

Many techniques for the verification of reactive systems rely on the analysis of their reachable state spaces. In this paper, a new algorithm for the symbolic generation of the state spaces of asynchronous system models, such as Petri nets, is developed. The algorithm is based on previous work that employs Multi-valued Decision Diagrams for efficiently storing sets of reachable states. In contrast to related approaches, however, it fully exploits event locality, supports intelligent cache management, and achieves faster convergence via advanced iteration control. The algorithm is implemented in the Petri net tool SMART, and run-time results show that it often performs significantly faster than existing state-space generators.

A. Miner, G. Ciardo, and S. Donatelli. Using the exact state space of a Markov model to compute approximate stationary measures. In J. Kurose and P. Nain, editors, Proceedings of the 2000 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems, pages 207-216. June 2000. ACM Press.

We present a new approximation algorithm based on an exact representation of the state space, using decision diagrams, and of the transition rate matrix, using Kronecker algebra, for a Markov model with K submodels. Our algorithm builds and solves K Markov chains, each corresponding to a different aggregation of the exact process, guided by the structure of the decision diagram, and iterates on their solution until their entries are stable. We prove that exact results are obtained if the overall model has a product-form solution. Advantages of our method include good accuracy, low memory requirements, fast execution times, and a high degree of automation, since the only additional information required to apply it is a partition of the model into the K submodels. As far as we know, this is the first time an approximation algorithm has been proposed where knowledge of the exact state space is explicitly used.

G. Ciardo and A. Miner. Structural approaches for SPN analysis. In A. Tenter, editor, High Performance Computing 2000, Grand Challenges in Computer Simulation, pages 345-356. Apr. 2000. SCS.

Petri nets and Markovian Petri nets are excellent tools for logic and performability system modeling. However, the size of the underlying reachability set is a major limitation in practice. One approach gaining attention among researchers is the use of structured representations, which require us to decompose a net into, or compose a net from, subnets. This paper surveys the state-of-the-art in advanced techniques for storing the reachability set and the transition rate matrix, with particular attention to the use of decision diagrams, Kronecker representations, and their interplay. The conclusion is that, in most practical applications, it is now possible to generate and store enormous reachability sets for logical analysis, while the size of the probability vector being sought is the main limitation when performing the exact solution of the underlying Markov chain.

G. Ciardo, A. Riska, and E. Smirni. An aggregation-based solution method for M/G/1-type processes. In W. Stewart and B. Plateau, editors, Numerical Solution of Markov Chains, pages 21-40, Sept. 1999. Prensas Universitarias de Zaragoza.

We extend the ETAQA approach, initially proposed for the efficient numerical solution of a class of quasi birth-death processes, to the more complex case of M/G/1-type Markov processes. The proposed technique can be used for the exact solution of a class of M/G/1-type models by computing the solution of a finite linear system. We further demonstrate the utility of the method by describing the exact computation of an extensive set of Markov reward functions such as the expected queue length or its higher moments. We illustrate the method, discuss its complexity, present comparisons with other traditional techniques, and illustrate its applicability in the area of computer system modeling.

G. Ciardo and A. Miner. A data structure for the efficient Kronecker solution of GSPNs. In P. Buchholz, editor, Proc. 8th Int. Workshop on Petri Nets and Performance Models (PNPM'99), pages 22-31. Sept. 1999. IEEE Comp. Soc. Press.

Kronecker-based approaches have been proposed for the solution of structured GSPNs with extremely large state spaces. Representing the transition rate matrix using Kronecker sums and products of smaller matrices virtually eliminates its storage requirements, but introduces various sources of overhead. We show how, by using a new data structure which we call matrix diagrams, we are able to greatly reduce or eliminate many of these overheads, resulting in a very efficient overall solution process.

A. Miner and G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In H. Kleijn and S. Donatelli, editors, Application and Theory of Petri Nets 1999, Lecture Notes in Computer Science 1639 (Proc. 20th Int. Conf. on Applications and Theory of Petri Nets, Williamsburg, VA, USA), pages 6-25. June 1999. Springer-Verlag.

We present a new technique for the generation and storage of the reachability set of a Petri net. Our approach is inspired by previous work on Binary and Multi-valued Decision Diagrams but exploits a concept of locality for the effect of a transition's firing to vastly improve algorithmic performance. The result is a data structure and a set of manipulation routines that can be used to generate and store enormous sets extremely efficiently in terms of both memory and execution time.

G. Ciardo and E. Smirni. Projection: An efficient solution algorithm for a class of quasi birth-death processes. In Proceedings of the Fourth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-4) , pages 58-61. Williamsburg, VA, USA, Sept. 1998.

Over the last two decades, considerable effort has been put into the development of matrix geometric techniques [Neuts, 1981] for the exact analysis of a general and frequently encountered class of queueing models that exhibit a regular structure. In these models, the embedded Markov chains are two-dimensional generalizations of elementary M/G/1 and G/M/1 queues [Kleinrock, 1975]. The intersection of these two cases corresponds to the so-called quasi-birth-death (QBD) processes. In this work, we develop an efficient methodology that can be used to compute performance measures for a class of QBD processes.

G. Li and G. Ciardo. Approximate analysis of a fault-tolerant join-the-shortest-queue policy. In Proceedings of the Fourth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-4), pages 34-38. Williamsburg, VA, USA, Sept. 1998.

In distributed or multi-processor systems, the join the shortest queue (JSQ) scheduling policy can provide competitive performance compared to other heuristic policies. However, processing nodes can fail. In order to provide fault tolerance, one proposed solution is using a ``buddy system''. We investigate a new scheduling system by combining these two methods together to provide good performance and high reliability. In this paper, we describe the system in detail and evaluate its performance using an approximation based on the matrix-geometric method. Our results show that our method provides very accurate estimates for the average number of jobs in the system.

G. Ciardo and G. Li. Efficient approximate transient analysis for a class of deterministic and stochastic Petri nets. In Proceedings of the IEEE International Computer Performance and Dependability Symposium (IPDS'98), pages 34-43. Durham, NC, USA, Sept. 1998. IEEE Computer Society Press.

Transient analysis of non-Markovian Stochastic Petri nets is a theoretically interesting and practically important problem. We present a new method to compute bounds and an approximation on the average state sojourn times for a special class of deterministic and stochastic Petri nets (DSPNs). In addition to the idea of the subordinated Markov chain traditionally used for the stationary solution of DSPNs, our algorithm makes use of concepts from renewal theory. An application to a finite-capacity queue with a server subject to breakdowns is included.

R. Zijal, G. Ciardo, and G. Hommel. Discrete deterministic and stochastic Petri nets. In Proc. ITG/GI-Fachtagung: Messung, Modellierung und Bewertung von Rechen- und Kommunikationssystemen (MMB'97), (Measurement, Modeling, and Valuation of Computer- and Communication-Systems), pages 103-117. Freiberg, Germany, Sept. 1997. VDE-Verlag.

Petri nets augmented with timing specifications gained a wide acceptance in the area of performance and reliability evaluation of complex systems exhibiting concurrency, synchronization, and conflicts. The state space of time-extended Petri nets is mapped onto its basic underlying stochastic process, which can be shown to be Markovian under the assumption of exponentially distributed firing times. The integration of exponentially and non-exponentially distributed timing is still one of the major problems for the analysis and was first attacked for continuous-time Petri nets at the cost of structural or analytical restrictions. We propose a discrete deterministic and stochastic Petri net (DDSPN) formalism with no imposed structural or analytical restrictions where transitions can fire either in zero time or according to arbitrary firing times that can be represented as the time to absorption in a finite absorbing discrete-time Markov chain (DTMC). Exponentially distributed firing times are then approximated arbitrarily well by geometric distributions. Deterministic firing times are a special case of the geometric distribution. The underlying stochastic process of a DDSPN is then also a DTMC, from which the transient and stationary solution can be obtained by standard techniques. A comprehensive algorithm and some state space reduction techniques for the analysis of DDSPNs are presented, including the automatic detection of conflicts and confusions, which removes a major obstacle for the analysis of discrete-time models.

G. Ciardo, D. Nicol, K. Trivedi. Discrete-event simulation of fluid stochastic Petri nets. In Proc. Int. Workshop on Petri Nets and Performance Models (PNPM'97), pages 217-225. June 1997. St. Malo, France, IEEE Comp. Soc. Press.

The purpose of this paper is to describe a method for simulation of recently introduced fluid stochastic Petri nets. Since such nets result in rather complex set of partial differential equations, numerical solution becomes a formidable task. Because of a mixed, discrete and continuous state space, simulative solution also poses some interesting challenges, which are addressed in the paper.

G. Ciardo and A. S. Miner. Storage alternatives for large structured state spaces. In Proc. 9th Int. Conf. on Modelling Techniques and Tools for Computer Performance Evaluation, LNCS 1245, pages 44-57. St. Malo, France, June 1997. Springer-Verlag.

We consider the problem of storing and searching a large state space obtained from a high-level model such as a queueing network or a Petri net. After reviewing the traditional technique based on a single search tree, we demonstrate how an approach based on multiple levels of search trees offers advantages in both memory and execution complexity. Further execution time improvements are obtained by exploiting the concept of ``event locality''. We apply our technique to three large parametric models, and give detailed experimental results.

G. Ciardo and A. S. Miner. SMART: Simulation and Markovian Analyzer for Reliability and Timing. In Proc. IEEE International Computer Performance and Dependability Symposium (IPDS'96), page 60, Urbana-Champaign, IL, USA, Sept. 1996. IEEE Comp. Soc. Press.

SMART is a new tool for performance, reliability, availability, and performability modeling. Numerical solution algorithms are available for both continuous- and discrete-time Markov chains. Mixed-time non-Markovian models can be studied using simulation. Multiple interacting models and fixed-point iterative techniques for the decomposition and solution of complex models can be easily specified. To assist in the model specification and help in avoiding common mistakes, the input language is strongly typed.

M. Tilgner, Y. Takahashi, and G. Ciardo. SNS 1.0: Synchronized Network Solver. In 1st International Workshop on Manufacturing and Petri Nets, pages 215-234. Osaka, Japan, June 1996.

We present SNS, a Solver for Synchronized Networks modelled as generalized stochastic Petri nets. General enabling and firing functions and reward measures are specified in the C programming language, providing extensive flexibility with respect to conventional net descriptions. Unstructured and structured steady-state and transient solutions are possible, to compute the specified rate-based and impulse-based reward measures. We allow the model to have both immediate and timed synchronizing transitions. Furthermore, the user can solve numerical linear algebra problems by a variety of algorithms based on solution vectors and matrices. We apply SNS on a case study of kanban systems and give numerical results. In the conclusion, we point out ideas to expand the package.

G. Ciardo and R. Zijal. Well-defined stochastic Petri nets. In Proc. 4th Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'96), pages 278-284. San Jose, CA, USA, Feb. 1996. IEEE Comp. Soc. Press.

Formalisms based on stochastic Petri Nets (SPNs) can employ structural analysis to ensure that the underlying stochastic process is fully determined. The focus is on the detection of conflicts and confusions at the net level, but this might require to overspecify a given SPN model. The problem becomes even more critical when reward processes of interest derived from the basic underlying process are considered. Typical examples are state-dependent impulse reward measures. We propose a definition of well-defined SPNs, which takes into account whether the basic underlying stochastic process or the derived reward processes are determined. A state-space-based algorithm to determine whether a given SPN is well-defined is provided.

G. Ciardo, L. Cherkasova, V. Kotov, and T. Rokicki. Modeling a scalable high-speed interconnect with stochastic Petri nets. In Proc. Int. Workshop on Petri Nets and Performance Models (PNPM'95), pages 83-92. Durham, NC, Oct. 1995, IEEE Comp. Soc. Press.

This paper presents an approach to using Stochastic Petri nets to model large-scale concurrent systems, in our case, a scalable computer interconnect. We show how Stochastic Petri net models can exploit the symmetry of the system to construct a tractable, but approximate, analytic model, and that they can yield results very close to those of a detailed simulation model, with much less computational effort.

G. Ciardo, L. Cherkasova, V. Kotov, and T. Rokicki. Modeling a fibre channel switch with stochastic Petri nets. In Proc. 1995 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, pages 319-320. Ottawa, Ontario, Canada May 1995.

As computing systems become increasingly complex and concurrent, performance analysis becomes more important, especially when designing an overall architecture. Simple numerical approximations can often yield bounds on performance. Queueing theory and Markovian analysis can provide insight into the steady-state performance of the system. Discrete-event simulation can provide a more detailed view of the system behavior. We used all of the above techniques in the performance study of a Fibre Channel switch. An approximate stochastic Petri net (SPN) model was employed, obtained by exploiting symmetries in the system. The most challenging aspect was determining transition firing probabilities that accurately reflected the dynamic behavior of the exact SPN. This model was valided against a detailed simulation and found to be accurate within 3%.

G. Ciardo. Discrete-time Markovian stochastic Petri nets. In W. J. Stewart, editor, Computations with Markov Chains, pages 339-358. Raleigh, NC, Jan. 1995. Kluwer.

We revisit and extend the original definition of discrete-time stochastic Petri nets, by allowing the firing times to have a ``defective discrete phase distribution''. We show that this formalism still corresponds to an underlying discrete-time Markov chain. The structure of the state for this process describes both the marking of the Petri net and the phase of the firing time for of each transition, resulting in a large state space. We then modify the well-known power method to perform a transient analysis even when the state space is infinite, subject to the condition that only a finite number of states can be reached in a finite amount of time. Since the memory requirements might still be excessive, we suggest a bounding technique based on truncation.

K. S. Trivedi, G. Ciardo, M. Malhotra, and S. Garg. Dependability and performability modeling using stochastic Petri nets. In Proc. 11th Int. Conf. on Analysis and Optimization of Systems - Discrete Event Systems, pages 144-157. Sophia-Antipolis, France, June 1994. Springer-Verlag.

This paper presents a tutorial on SPNs and their use for the analysis of dependability and performability measures. The main limitations of SPNs, the size of the state space and the assumption of exponentially distributed firing times, are also addressed.

G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In R. Valette, editor, Application and Theory of Petri Nets 1994, Lecture Notes in Computer Science 815 (Proc. 15th Int. Conf. on Applications and Theory of Petri Nets,, pages 179-198. Zaragoza, Spain June 1994. Springer-Verlag,

We discuss P/T-nets where the arc cardinalities are allowed to be marking-dependent expressions of various types, resulting in a hierarchy of subclasses. Some of the language and decidability properties of these classes have been studied before, but we focus on the practical implications in systems modeling, adding some new insight to the known results about the relative expressive power of the subclasses. We show how the p-semiflows of a P/T-net with marking-dependent arc cardinality can be obtained from the p-semiflows of a related ordinary P/T-net and how bounds on the relative throughputs of the transitions can be obtained, a weaker condition than t-semiflows. Finally, we briefly discuss several modeling applications where these subclasses are used.

G. Ciardo, R. German, and C. Lindemann. A characterization of the stochastic process underlying a stochastic Petri net. In Proc. 5th Int. Workshop on Petri Nets and Performance Models (PNPM'93), pages 170-179. Toulouse, France, Oct. 1993. IEEE Comp. Soc. Press.

Stochastic Petri nets (SPNs) with generally distributed firing times are isomorphic to generalized semi-Markov processes (GSMPs), but simulation is the only feasible approach for their solution. We explore a hierarchy of SPN classes where modeling power is reduced in exchange for an increasingly efficient solution. Generalized stochastic Petri nets (GSPNs), deterministic and stochastic Petri nets (DSPNs), semi-Markovian stochastic Petri nets (SM-SPNs), timed Petri nets (TPNs), and generalized timed Petri nets (GTPNs) are particular entries in our hierarchy. Additional classes of SPNs for which we show how to compute an analytical solution are obtained by the method of the embedded Markov chain (DSPNs are just one example in this class) and state discretization, which we apply not only to the continuous-time case (PH-type distributions), but also to the discrete case.

G. Ciardo and C. Lindemann. Analysis of deterministic and stochastic Petri nets. In Proc. 5th Int. Workshop on Petri Nets and Performance Models (PNPM'93), pages 160-169. Toulouse, France, Oct. 1993. IEEE Comp. Soc. Press.

We present a time and space efficient algorithm for computing steady state solutions of deterministic and stochastic Petri nets (DSPNs) with both stochastic and structural extensions. The algorithm can deal with different execution policies associated with deterministic transitions of a DSPN. The definition of a subordinated Markov chain (SMC) is refined to reduce the computational cost of deriving the transition probabilities of the embedded Markov chain (EMC) underlying a DSPN. Closed-form expressions of these transition probabilities are presented for some SMC topologies. Moreover, we propose to make use of the reward structure defined on the DSPN to reduce memory requirements. The usefulness of the proposed extensions and the steps of the solution algorithm are illustrated using a DSPN of a simple communication protocol.

C. Lindemann, G. Ciardo, R. German, and G. Hommel. Performability modeling of an automated manufacturing system with deterministic and stochastic Petri nets. In Proc. 1993 IEEE Int. Conf. on Robotics and Automation, pages 576-581. Atlanta, GA, May 1993. IEEE Press.

In this paper we present a Deterministic and Stochastic Petri Net model for an automated manufacturing system in which tools are subject to wear and maintenance. The DSPN takes into account the degradable performance of tools due to wear and the deterministic service times of parts. The service requirements of parts at tools dependent on their wear are represented in the DSPN by deterministic transitions with marking-dependent firing delays. The DSPN is employed for an integrated performance/dependability evaluation of the considered automated manufacturing system.

J. K. Muppala, G. Ciardo, and K. S. Trivedi. Modeling using Stochastic Reward Nets. In Proc. 1st Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'93), pages 367-372. San Diego, CA, USA, Jan. 1993. IEEE Comp. Soc. Press.

In this paper we describe the modeling of complex systems using stochastic reward nets (SRNs) which are stochastic Petri nets (SPNs) augmented with the ability to specify output measures as reward based functions. The solution of the SRNs involves generation and solution of the corresponding Markov reward model. Several structural extensions to SPNs, including marking dependency, variable cardinality arcs and guards which are useful in modeling the complex behavior of systems, are described. The use of SRNs in modeling complex systems is illustrated through an interesting example.

G. Ciardo and K. S. Trivedi. Solution of large GSPN models. In W. J. Stewart, editor, Numerical Solution of Markov Chains, pages 565-595. Marcel Dekker, Inc., New York, NY, 1991.

Generalized Stochastic Petri Nets (GSPNs) can be effectively used to represent many systems in a compact way. Efficient algorithms for the translation of a GSPN into its underlying Continuous Time Markov Chain (CTMC) are known and have been implemented in a number of software packages. While GSPNs relieve the modeler from the cumbersome and error-prone task of building and inputting the CTMC by hand, their analytical tractability is still limited by the combinatorial growth of the underlying CTMC. In order to avoid construction and solution of a large CTMC, we propose decomposing the GSPN into a set of subnets and separately solving individual subnets. Dependence among the subnets requires that, after solving each subnet, certain quantities be exported to other subnets. A fixed-point iteration is then used over the exported quantities. We discuss ways of decomposing a net into subnets, the type of quantities that need to be exchanged between subnets, and the convergence of the fixed-point iterative schemes.

G. Ciardo and K. S. Trivedi. A decomposition approach for stochastic Petri net models. In Proc. 4th Int. Workshop on Petri Nets and Performance Models (PNPM'91), pages 74-83. Melbourne, Australia, Dec. 1991. IEEE Comp. Soc. Press.

We present a decomposition approach for the solution of large stochastic Petri nets (SPNs). The overall model consists of a set of submodels whose interactions are described by an import graph. Each node of the graph corresponds to a parametrized SPN submodel and an arc from submodel A to submodel B corresponds to a parameter value that B must receive from A. The quantities exchanged between submodels are based on only three primitives. The import graph is normally cyclic, so the solution method is based on fixed point iteration. We apply our technique to the analysis of a flexible manufacturing system.

G. Ciardo, K. S. Trivedi, and J. K. Muppala. SPNP: stochastic Petri net package. In Proc. 3rd Int. Workshop on Petri Nets and Performance Models (PNPM'89), pages 142-151. Kyoto, Japan, Dec. 1989. IEEE Comp. Soc. Press.

We present SPNP, a powerful GSPN package developed at Duke University. SPNP allows the modeling of complex system behaviors. Advanced constructs are available, such as marking-dependent arc multiplicities, enabling functions, arrays of places or transitions, and subnets; in addition, the full expressive power of the C programming language is available to increase the flexibility of the net description. Sophisticated steady-state and transient solvers are available; cumulative and up-to-absorption measures can be computed. In addition, the user is not limited to a predefined set of measures: detailed expressions reflecting exactly the measures sought can be easily specified. We conclude comparing SPNP with two other SPN-based packages, GreatSPN and METASAN.

G. Ciardo. Toward a definition of modeling power for stochastic Petri net models. In Proc. Int. Workshop on Petri Nets and Performance Models (PNPM'87), pages 54-62. Madison, Wisconsin, Aug. 1987. IEEE Comp. Soc. Press.

Some insight on the meaning of ``modeling power'' for Stochastic Petri Net models is given. Extensions characterizing a Stochastic Petri Net are categorized as logical or stochastic. Three logical constructs are shown to be equivalent: inhibitor arcs, transition priorities, and enabling functions associated with the transitions. A direct transformation of Petri Nets with inhibitor arcs into Petri Nets with transition priorities and vice versa is given, determining a bound on the size of equivalent nets in the two models. As a consequence, the higher priority of immediate transitions over timed transitions in the GSPN model is shown to provide the full power of Turing machines.

J. Bechta Dugan and G. Ciardo. Stochastic Petri net analysis of a replicated file system. In Proc. Int. Workshop on Petri Nets and Performance Models (PNPM'87), pages 84-92. Madison, Wisconsin, Aug. 1987. IEEE Comp. Soc. Press.

We present a stochastic Petri net model of a replicated file system in a distributed environment. Replicated files are assumed to reside on different hosts and use a voting algorithm to maintain consistency. Witnesses, which simply record the status of the file but contain no data, may be used to reduce overhead. We present a model sufficiently detailed to include file status (current or out of date) as well as failure and repair of hosts where copies or witnesses reside. The number of copies and witnesses is not fixed, but is a parameter of the model. Two different majority protocols are examined, one where a majority of all copies and witnesses is necessary to form a quorum, the other where only a majority of the copies and witnesses on operational hosts is needed. The latter, known as adaptive voting, is shown to increase file availability. We also investigate the process of selection of copies and witnesses to participate in an update when more than the majority is available.

K. S. Trivedi, G. Ciardo, and J. Bechta Dugan. Dependability evaluation of fault-tolerant multiple processor systems. In N. A. E. Ata, editor, Modelling Techniques and Tools for Performance Analysis '85. Elsevier Science Publishers B.V. (North-Holland), 1986. Invited.

We present an overview of the major problems inherent in dependability modeling of fault tolerant multiple processor systems, and discuss the solution approaches often used. References are provided to many of the important techniques utilized in reliability, availability, and performance modeling of such systems.

J. Bechta Dugan, A. Bobbio, G. Ciardo, and K. Trivedi. The design of a unified package for the solution of stochastic Petri net models. In Proc. Int. Workshop on Timed Petri Nets, pages 6-13. Torino, Italy, July 1985. IEEE Comp. Soc. Press.

M. Ajmone Marsan, G. Balbo, G. Ciardo, and G. Conte. A software tool for the automatic analysis of Generalized Stochastic Petri Net models. In D. Potier, editor, Modelling Techniques and Tools for Performance Analysis, pages 155-170. INRIA, Elsevier Science Publishers B.V. (North-Holland), June 1985.

G. Ciardo and C. Iacobelli. On the relational-CODASYL query translatability. In Proc. 2nd Convencion Informatica Latina, Barcelona, Spain, April 1985.

M. Bert, G. Ciardo, M. L. Demarie, C. Iacobelli, and P. Marchisio. A relational interface for CODASYL databases. In Proc. Congr. ``Making Database Work - Trends and Applications'', pages 707-712. Gaithersburg, Maryland, May 1984. IEEE and NBS.

G. Ciardo. Data representation and efficient solution: a decision diagram approach. In M. Bernardo and J. Hillston, editors, Formal Methods for Performance Evaluation, LNCS 4486, pages 371-394. Springer-Verlag, 2007.

Decision diagrams are a family of data structures that can compactly encode many functions on discrete structured domains, that is, domains that are the cross-product of finite sets. We present some important classes of decision diagrams and show how they can be effectively employed to derive ``symbolic'' algorithms for the analysis of large discrete-state models. In particular, we discuss both explicit and symbolic algorithms for state-space generation, CTL model-checking, and continuous-time Markov chain solution. We conclude with some suggestions for future research directions.

G. Ciardo. Distributed and structured analysis approaches to study large and complex systems. In E. Brinksma, H. Hermanns, and J.-P. Katoen, editors, Lectures on Formal Methods and Performance Analysis, LNCS 2090, pages 344-374. Springer-Verlag, 2001.

Both the logic and the stochastic analysis of discrete-state systems are hindered by the combinatorial growth of the state space underlying a high-level model. In this work, we consider two orthogonal approaches to cope with this ``state-space explosion''. Distributed algorithms that make use of the processors and memory overall available on a network of N workstations can manage models with state spaces approximately N times larger than what is possible on a single workstation. A second approach, constituting a fundamental paradigm shift, is instead based on decision diagrams and related implicit data structures that efficiently encode the state space or the transition rate matrix of a model, provided that it has some structure to guide its decomposition; with these implicit methods, enormous sets can be managed efficiently, but the numerical solution of the stochastic model, if desired, is still a bottleneck, as it requires vectors of the size of the state space.

G. Ciardo. Tools for formulating Markov models. In W. Grassmann, editor, Computational Probability, Operations Research and Management Science Series, Vol. 24, pages 11-41. Kluwer, 1999.

Markov models are used to study a wide class of systems. In this chapter, we restrict ourselves to Markov chains (MCs), that is, Markov models with a discrete state space, normally assumed to be a subset of the natural numbers. We discuss mostly continuous-time MCs (CTMCs), but we occasionally refer to discrete-time MCs (DTMCs).

G. Ciardo. Stochastic Petri Nets: Introduction and Applications to the Modeling of Computer and Communication Systems. In K. Bagchi, J. Walrand, and G. Zobrist, editors, State-of-the Art in Performance Modeling and Simulation: Advanced Computer Systems, pages 203-234. Gordon and Breach, 1998.

Starting from the basic Petri net definition, we consider SPN's having an underlying CTMC or DTMC, respectively. Then, we move to more sophisticated classes of SPNs having underlying processes which are either semi-Markov or Markov-regenerative. Finally, we survey more specialized areas of recent SPN research. Running examples are used throughout the presentation, and appropriate bibliographic citations are given.

K. S. Trivedi, G. Ciardo, M. Malhotra, and R. Sahner. Dependability and Performability Analysis. In L. Donatiello and R. Nelson, editors, Performance Evaluation of Computer and Communications Systems, Lecture Notes in Computer Science 729, pages 587-612. Springer-Verlag, 1993.

In this tutorial, we discuss several practical issues regarding specification and solution of dependability and performability models. We compare model types with and without rewards. Continuous-time Markov chains (CTMCs) are compared with (continuous-time) Markov reward models (MRMs) and generalized stochastic Petri nets (GSPNs) are compared with stochastic reward nets (SRNs). It is shown that reward-based models could lead to more concise model specification and solution of a variety of new measures. With respect to the solution of dependability and performability models, we identify three practical issues: largeness, stiffness, and non-exponentiality, and we discuss a variety of approaches to deal with them, including some of the latest research efforts.

G. Ciardo, A. Blakemore, P. F. J. Chimento, J. K. Muppala, and K. S. Trivedi. Automated generation and analysis of Markov reward models using Stochastic Reward Nets. In C. Meyer and R. J. Plemmons, editors, Linear Algebra, Markov Chains, and Queueing Models, volume 48 of IMA Volumes in Mathematics and its Applications, pages 145-191. Springer-Verlag, 1993.

Markov and Markov reward models are widely used for the performance and reliability analysis of computer and communication systems. Models of real systems often contain thousands or even millions of states. We propose the use of Stochastic Reward Nets (SRNs) for the automatic generation of these large Markov reward models. SRNs do allow the concise specification of practical performance, reliability and performability models. An added advantage of using SRNs lies in the possibility of analyzing the (time-independent) logical behavior of the modeled system. This helps both the validation of the system (is the right system being built?) and of the model (does the model correctly represent the system?). We discuss the methods to convert SRNs into Markov reward processes automatically. We review the solution techniques for the steady state and transient analysis of SRNs and Markov reward processes. We also discuss methods for the sensitivity analysis of SRNs.

M. Bert, G. Ciardo, B. Demo, A. Di Leva, P. Giolito, C. Iacobelli, and V. Marrone. The logical design in the DATAID project: the EASYMAP system. In A. Albano, V. De Antonellis, and A. Di Leva, editors, Computer Aided Database Design. North-Holland, 1985.

G. Ciardo. Modeling and analysis of Markov chains using decision diagrams. In Tutorials of QEST'04, Enschede, The Netherlands. Sept. 2004.

G. Ciardo, R. L. Jones, R. M. Marmorstein, A. S. Miner, and R. Siminiceanu. SMART: Stochastic Model-checking Analyzer for Reliability and Timing. In Proc. International Conference on Dependable Systems and Networks (DSN), page 545, Washington, D.C., USA. June 2002. IEEE Comp. Soc. Press.

G. Ciardo, R. German, and B. Haverkort. Introduction to the special section on Petri nets and performance models. IEEE Trans. Softw. Eng., 28(10):913-914, Oct. 2002.

G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. SMART: Stochastic Model Analyzer for Reliability and Timing In Tools of Aachen 2001 International Multiconference on Measurement, Modelling and Evaluation of Computer-Communication Systems, pages 29-34. Aachen, Germany, Sept. 2001.

SMART is a software package that integrates various logic and stochastic modeling formalisms into a single environment. Models expressed in different formalisms can be combined in the same study. For the analysis of the logical behavior, both explicit and symbolic state-space generation techniques, as well as CTL model checking algorithms, are available. For the study of the stochastic and timing behavior, both explicit and Kronecker numerical solution approaches are available, in addition to simulation. Since SMART is intended as an industry tool and a research tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.

G. Ciardo and A. S. Miner. SMART: Simulation and Markovian Analyzer for Reliability and Timing. In Tools Descriptions from the 9th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation and the 7th International Workshop on Petri Nets and Performance Models, pages 41-43. Saint Malo, France, June 1997.

SMART is a new tool designed to allow various high-level stochastic modeling formalisms (such as stochastic Petri nets and queueing networks) to be described in a uniform environment and solved using a variety of solution techniques, including numerical methods and simulation. Since SMART is intended as a research tool, it is written in a modular way that permits the easy integration of new solution algorithms.

G. Ciardo and C. Ghezzi. Guest Editorial: Introduction to the Special Section. IEEE Trans. Softw. Eng., 22(9):601-602, Sept. 1996.

H. Beilner, G. Ciardo, C. Lindemann, and K. Trivedi, editors. Performance and Dependability Modelling with Stochastic Petri Nets, Saarbrucken, Germany, May 1995. IBFI GmbH, Schloss Dagstuhl. Dagstuhl-Seminar-Report 115 - 22.05.-26.05.95 (9521).

K. Trivedi, A. Bobbio, G. Ciardo, R. German, A. Puliafito, and M. Telek. Non-Markovian Petri nets. In Proc. 1995 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, pages 263-264. Ottawa, Ontario, Canada, May 1995.

G. Ciardo, L. Cherkasova, V. Kotov, and T. Rokicki. Modeling a fibre channel switch with stochastic Petri nets. HP Labs Technical Report, Hewlett Packard, Palo Alto, CA, Nov. 1994.

G. Ciardo. Stochastic Petri nets: a formalism to describe stochastic processes. In Tutorials 1994 ACM SIGMETRICS Conf. on Measurement and Modeling of Computer Systems, Nashville, TN, May 1994.

G. Ciardo and K. S. Trivedi. SPNP: The Stochastic Petri Net Package (Version 3.1). In Proc. 1st Int. Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS'93), pages 390-391. San Diego, CA, USA, Jan. 1993. IEEE Comp. Soc. Press.

G. Ciardo. PNPM'91 - 4th International Workshop on Petri Nets and Performance Models. Perf. Eval., 18(1):97-100, 1993.

K. S. Trivedi and G. Ciardo. Putting Stochastic Petri Nets to Work. VHS videotape (5 hours), University of Southern California for the National Television University, May 1991.

G. Ciardo. Analysis of large stochastic Petri net models. PhD thesis, Duke University, Durham, NC, 1989.

Here is an errata.

G. Ciardo. Le reti di Petri stocastiche generalizzate: uno strumento per la modellizzazione di sistemi distribuiti. Tesi di Laurea, Istituto di Scienze dell' Informazione, Universita' di Torino, Italy, July 1982.