Gianfranco Ciardo's Publications
Publications are listed in reverse chronological order
(most recent first) within the following categories:
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.
Journal Papers
M. Mumme and G. Ciardo.
An efficient fully symbolic bisimulation algorithm
for nondeterministic systems.
Int. J. Foundations of Computer Science, 24(2):263282, 2013.

The definition of bisimulation suggests a partitionrefinement step,
which we show to be suitable for a saturationbased implementation.
We compare our fully symbolic saturationbased implementation with the
fastest extant bisimulation algorithms over a set of benchmarks,
and conclude that it appears to be the fastest algorithm capable of computing
the largest bisimulation over very large quotient spaces.
A. Graner et al.
A physical, genetical and functional sequence assembly of the barley genome.
Nature, 491:711717, 2012

Barley (Hordeum vulgare L.) is amongst the world's earliest domesticated and most important crop plants. It is diploid with a large haploid genome of 5.1 gigabases (Gb). Here we present an integrated and ordered physical, genetical and functional sequence resource that describes the barley genespace in a structured wholegenome context. We developed a physical map of 4.98 Gb, more than 3.90 Gb anchored to a highresolution genetic map. Projecting a deep wholegenome shotgun (WGS) assembly, cDNA and RNAseq data onto this framework supports 79,379 transcript clusters including 26,159 'high confidence' (HC) genes with homology support from other plant genomes. Abundant alternative splicing (AS), premature termination codons (PTCs) and novel transcriptionally active regions (nTARs) suggest posttranscriptional processing forms an important regulatory layer, and survey sequences from diverse accessions reveal a landscape of extensive single nucleotide variation (SNV). Our data provides a platform for both genomeassisted research and enabling contemporary crop improvement.
G. Ciardo, Y. Zhao, and X. Jin.
Ten years of saturation: a Petri net perspective.
Transactions on Petri Nets and Other Models of Concurrency, V:5195, 2012.

Due to their appealing conceptual simplicity and availability of
computer tools for their analysis, Petri nets are widely used
to model discreteevent systems in many areas of engineering.
However, the computational resources required to carry out the analysis of a
Petri net model are often enormous, hindering their practical impact.
In this survey, we consider how symbolic methods based on the use
of decision diagrams can greatly increases the
size of Petri nets that an ordinary computer can reasonably tackle.
In particular, we present this survey from the perspective of the
efficient saturation method we proposed a decade ago, and
introduce along the way the most appropriate classes of decision diagrams
to answer important Petri net questions, from reachability to
CTL model checking and counterexample generation,
from psemiflow computation to the solution of timed or Markovian nets.
Y. Zhang and G. Ciardo.
Symbolic computation of strongly connected components
and fair cycles using saturation.
Innovations in Systems and Software Engineering, 7(2):141150, 2011.

The computation of strongly connected components (SCCs) in discretestate models is a
critical step in formal verification of LTL and fair CTL properties, but the potentially huge number of
reachable states and SCCs constitutes a formidable challenge. We consider the problem of computing
the set of states in SCCs or terminal SCCs in an asynchronous system. We employ the idea of saturation,
which has shown clear advantages in symbolic statespace exploration, to improve two previously
proposed approaches: we use saturation to speed up state exploration when computing each SCC in
the XieBeerel algorithm, and we compute the transitive closure of the transition relation using a novel
algorithm based on saturation. Furthermore, we show that the techniques we developed are also
applicable to the computation of fair cycles. Experimental results indicate that the improved
algorithms using saturation achieve a substantial speedup over previous BFSbased algorithms. In
particular, with the new transitive closure computation algorithm can explore up to 10^150 SCCs
within a few seconds.
M. Wan, G. Ciardo, and A. S. Miner.
Approximate steadystate analysis of large Markov models
based on the structure of their decision diagram encoding.
Performance Evaluation, 68:463486, 2011.

We propose a new approximate numerical algorithm for the steadystate solution
of general structured ergodic Markov models.
The approximation uses a statespace encoding based on multiway decision
diagrams and a transition rate encoding based on a new
class of edgevalued decision diagrams.
The new method retains the favorable properties of a previously
proposed Kroneckerbased approximation, while eliminating the need
for a Kroneckerconsistent model decomposition.
Removing this restriction allows for a greater utilization of event
locality, which facilitates the generation of both the statespace
and the transition rate matrix, thus extends the
applicability of this algorithm to larger and more complex models.
G. Ciardo, A. S. Miner, and M. Wan.
Advanced features in SMART: the Stochastic Model checking Analyzer
for Reliability and Timing.
Performance Evaluation Review, 36(4):5863, 2009.

We describe some of the advanced features of the software tool SMART,
the Stochastic Model checking Analyzer for Reliability and Timing.
Initially conceived as a software package for numerical solution and
discreteevent simulation of stochastic models, SMART now also provides
powerful modelchecking capabilities, thanks to its extensive use
of various forms of decision diagrams, which in turn also greatly increase the
efficiency of its stochastic analysis algorithms.
These aspects make it an excellent choice when tackling systems with
extremely large state spaces.
A. J. Yu, G. Ciardo, and G. Luettgen.
Decisiondiagrambased techniques for bounded reachability checking
of asynchronous systems.
Software Tools for Technology Transfer, 11(2):117131, Apr. 2009.

Bounded reachability analysis and bounded model checking are widely
believed to perform poorly when using decision diagrams instead of
SAT procedures. Recent research suggests this to be untrue with
regards to synchronous systems and, in particular, digital circuits.
This article shows that the belief is also a myth for asynchronous
systems, such as models specified by Petri nets. We propose several
Bounded Saturation approaches to compute bounded state spaces
using decision diagrams. These approaches are based on the
established Saturation algorithm, which benefits from a nonstandard
search strategy that is very different from breadthfirst search,
but employ different flavors of decision diagrams: Multivalued
Decision Diagrams, Edgevalued Decision Diagrams, and Algebraic
Decision Diagrams. We apply our approaches to studying deadlock as
a safety property. Our extensive benchmarking shows that our
algorithms often, but not always, compare favorably against two
SATbased approaches that are advocated in the literature.
M.Y. Chung and G. Ciardo.
Speculative image computation for distributed symbolic reachability analysis.
Journal of Logic and Computation, doi=10.1093/logcom/exp005,
Oxford University Press, 2009.

The Saturationstyle fixpoint iteration strategy for symbolic reachability
analysis is particularly effective for globallyasynchronous
locallysynchronous discretestate systems.
However, its inherently sequential nature makes it difficult
to parallelize Saturation on a NOW.
We then propose the idea of using idle workstation time to perform
speculative image computations.
Since an unrestrained prediction may make excessive use of computational
resources, we introduce a historybased approach to dynamically recognize
image computation (event firing) patterns and explore only firings
that conform to these patterns.
In addition,
we employ an implicit encoding for the patterns,
so that the actual image computation history can be efficiently preserved.
G. Ciardo, Y. Zhao, and X. Jin.
Parallel symbolic statespace exploration is difficult,
but what is the alternative?
In EPTCS,
14:117, 2009

Statespace exploration is an essential step in many modeling and analysis problems. Its goal is to find the states reachable from the initial state of a discretestate model described. The state space can used to answer important questions, e.g., "Is there a dead state?" and "Can N become negative?", or as a starting point for sophisticated investigations expressed in temporal logic.
Unfortunately, the state space is often so large that ordinary explicit data structures and sequential algorithms cannot cope, prompting the exploration of (1) parallel approaches using multiple processors, from simple workstation networks to sharedmemory supercomputers, to satisfy large memory and runtime requirements and (2) symbolic approaches using decision diagrams to encode the large structured sets and relations manipulated during statespace generation.
Both approaches have merits and limitations. Parallel explicit statespace generation is challenging, but almost linear speedup can be achieved; however, the analysis is ultimately limited by the memory and processors available. Symbolic methods are a heuristic that can efficiently encode many, but not all, functions over a structured and exponentially large domain; here the pitfalls are subtler: their performance varies widely depending on the class of decision diagram chosen, the state variable order, and obscure algorithmic parameters.
As symbolic approaches are often much more efficient than explicit ones for many practical models, we argue for the need to parallelize symbolic statespace generation algorithms, so that we can realize the advantage of both approaches. This is a challenging endeavor, as the most efficient symbolic algorithm, Saturation, is inherently sequential. We conclude by discussing challenges, efforts, and promising directions toward this goal.
G. Ciardo.
Decision diagrams for the approximate analysis of Markov models.
Wiley Interscience (online journal), 7(1):10807051080706, Dec. 2008.

Decision diagrams of various types can be used to encode the exact state
space and transition rate matrix of large Markov models. However, the
exact solution of such models still requires to store at least one real
vector with one entry per reachable state, a formidable limitation
to the practical use of these encodings. Thus, we discuss automatic
techniques for the approximate computation of performance measures
when the Markov model can be compactly encoded but not exactly solved.
R. Siminiceanu and G. Ciardo.
Formal verification of the NASA Runway Safety Monitor.
Software Tools for Technology Transfer, 9(1):6376, 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 statespace 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 realworld 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 statespace generation.
Formal Methods in System Design, 31:63100, 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 statespace exploration
techniques using decision diagrams can be drastically improved by
exploiting the interleaving semantics underlying many eventbased
and componentbased system models. A new algorithm for symbolically
generating state spaces is presented that (i) encodes a model's
state vectors with Multivalued Decision Diagrams (MDDs)
rather than flattening them into BDDs and (ii) partitions the model's
Kroneckerconsistent nextstate function by event and
subsystem, thus enabling multiple lightweight nextstate
transformations rather than a single heavyweight one. Together,
this paves the way for a novel iteration order, called
saturation, which replaces the breadthfirst 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):425, 2006.

We present various algorithms for generating the state space of an
asynchronous system, based on the use of multiway decision diagrams
to encode sets and Kronecker operators on boolean matrices to encode
the nextstate 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 breadthfirst 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 ``onthefly'' explicit
statespace generation of each submodel
with symbolic statespace 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:578608, 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
statespace generation techniques, as well as symbolic CTL modelchecking
algorithms, are available.
For the study of stochastic and timing behavior, both
sparsestorage and Kronecker numerical solution approaches are available
when the underlying process is a Markov chain.
In addition, discreteevent simulation is always applicable regardless
of the stochastic nature of the process, but
certain classes of nonMarkov 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. S. Miner.
Implicit data structures for logic and stochastic systems analysis.
Performance Evaluation Review, 32(4):49, 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.
Workloadaware load balancing for clustered web servers.
IEEE Trans. Par. and Distr. Syst., 16(3):219233. Mar. 2005.

We focus on load balancing policies for homogeneous clustered web servers that
tune their parameters onthefly to adapt to
changes in the arrival rates and service times of incoming requests.
The proposed scheduling policy, AdaptLoad, monitors the incoming workload
and selfadjusts 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 online 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 localityaware 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.
ETAQAMG1: An efficient technique for the analysis
of M/G/1type processes by aggregation.
Performance Evaluation, 57(3):235260. July 2004.

We extend the ETAQA approach, initially proposed
for the efficient numerical solution of a class of
quasi birthdeath processes,
to a more complex class of M/G/1type 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/1type 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/1type performability models.
IEEE Trans. Rel., 53(2):238249, June 2004.

We present an exact decomposition algorithm for the analysis
of Markov chains with a GI/G/1type repetitive structure.
Such processes exhibit both M/G/1type and GI/M/1type 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 aggregationbased method for the
exact analysis of a class of GI/G/1type processes.
Performance Evaluation Review, 31(2):2830, Sept. 2003.

We present an aggregationbased algorithm for the
exact analysis of Markov chains with GI/G/1type pattern
in their repetitive structure, i.e., chains that exhibit
both M/G/1type and GI/M/1type 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/1type or the GI/M/1type, or their intersection, i.e.,
quasibirthdeath processes.
G. Ciardo, A. Riska, and E. Smirni.
EQUILOAD: a load balancing policy for clustered web servers.
Performance Evaluation, 46(23):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 backend servers, and its parameters
are obtained from the analysis of a trace's past data.
To study its performance, we use phasetype 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 backend servers, therefore behaving
similarly to a ``localityaware'' allocation policy, but at a very
low implementation cost.
P. Buchholz, G. Ciardo, P. Kemper, and S. Donatelli.
Complexity of memoryefficient 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 shufflebased
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 Jacobistyle and GaussSeidelstyle 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 QBDprocesses by Aggregation
Perf. Eval., 3637:7193, 1999.

In this paper we present ETAQA,
an Efficient Technique for the Analysis of QBDprocesses 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.
Discreteevent simulation of fluid stochastic Petri nets.
IEEE Trans. Softw. Eng., 25(2):207217, 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:109129, 1999.

Transient analysis of nonMarkovian 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 finitecapacity queue with a
server subject to breakdowns, and assess the quality of our approximations.
G. Ciardo, J. Gluckman, and D. Nicol.
Distributed statespace generation of discretestate stochastic models.
INFORMS J. Comp., 10(1):8293, 1998.

Highlevel 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
onthefly 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
multicomputer.
D. Nicol and G. Ciardo.
Automated parallelization of discrete statespace generation.
Journal of Parallel and Distributed Computing,
47:153167, 1997.

We consider the problem of generating a large statespace 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:313326, 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 selfstabilizing clock synchronization by
means of stochastic Petri nets''.
IEEE Trans. Comp., 43(12):14531456, Dec. 1994.

We correct some problems in the approach presented
by Lu, Zhang, and Murata in their paper ``Analysis of selfstabilizing
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):920, 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 rewardbased
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):506515, 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),
semiMarkovian stochastic Petri nets (SMSPNs),
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 continuoustime
case (PHtype 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):3759, 1993.

We present a decomposition approach for the solution of
large stochastic reward nets (SRNs) based on the concept of nearindependence.
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 nearlyindependent 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 faulttolerant software using stochastic Petri nets.
J. Par. and Distr. Comp., 15(3):255269, July 1992.

We present two software applications and develop models for them.
The first application considers a producerconsumer 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 faulttolerant
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
steadystate 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):237253, 1991.

We extend the basic GSPN (generalized stochastic Petri net) model
to GSPNreward 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 steadystate solution of
GSPN models,
based on the correspondence between GSPNs and continuoustime Markov chains
(CTMCs), is compared with a method based on
discretetime Markov chains (DTMCs) previously judged poor.
We show that there are GSPNs when the DTMCbased 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 semiMarkov reward processes.
IEEE Trans. Comp., 39(10):12511264, Oct. 1990.

With the increasing complexity of multiprocessor and distributed processing
systems, the need to develop efficient and accurate modeling methods is evident.
Faulttolerance 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 semiMarkov 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 semiMarkov 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
faulttolerant 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.

Continuoustime 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):394401, 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 outofdate) 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.
Conference Papers
X. Jin, A. Donze', and G. Ciardo.
Mining weighted requirements from closedloop control models.
In Proc. Numerical Software Verification,
pages 4751.
2013.

Specification defects are a major source of ambiguities and errors.
We propose a new weighted requirement mining framework to address this problem.
We define weighted and parametric weighted signal temporal logic (STL)
as the underlying formalism to improve the expressiveness.
This also improves convergence of the mining process. We provide some primitive
results to show the benefit of the new framework.
Y. Zhao and G. Ciardo.
Tackling truncation errors in CSL model checking through bounding semantics.
In Proc. EPEW,
LNCS 8168, pages 5873.
2013.

Model checking aims to give exact answers to queries about a model's
execution but, in probabilistic model checking, ensuring exact answers
might be difficult.
Numerical iterative methods are heavily used in probabilistic model checking
and errors caused by truncation may affect correctness.
To tackle truncation errors, we investigate the bounding semantics of
\emph{continuous stochastic logic} for Markov chains.
We first focus on analyzing truncation errors for modelchecking the
timebounded or unbounded Until operator and propose new algorithms
to generate lower and upper bounds.
Then, we study the bounding semantics for a subset of nested CSL formulas.
We demonstrate result on two models.
X. Jin, Y, Lembachar, and G. Ciardo.
Symbolic verification of ECA rules
In Joint Proc. PNSE'13 and ModBE'13,
CEUR 989,
pages 4159.
2013.

Eventconditionaction (ECA) rules specify
a decision making process and are widely used in reactive systems and active
database systems.
Applying formal verification techniques to guarantee
properties of the designed ECA rules is essential to help
the errorprone procedure of collecting and translating expert knowledge.
The nondeterministic and concurrent semantics of ECA rule execution
enhance expressiveness but hinder analysis and verification.
We then propose an approach to analyze the dynamic
behavior of a set of ECA rules,
by first translating them into an extended Petri net, then studying
two fundamental correctness properties:
termination and confluence.
Our experimental results show that the symbolic algorithms we present
greatly improve scalability.
Y. Zhao and G. Ciardo.
A twophase GaussSeidel algorithm for steadystate solution of
structured CTMCs encoded with EVMDDs.
In Proc. QEST,
pages 7483.
2012.

We present a new symbolic approach for the steadystate solution of ergodic
continuoustime Markov chains (CTMCs) using iterative methods, based
on EdgeValued Multiway Decision Diagrams~(EVMDDs) to store an indexing
function for the structured states and the transition rate matrix.
The approach is applicable to any structured CTMC,
is memory efficient, and supports both Jacobi and GaussSeidel iterations.
In particular, our main contribution is a new twophase algorithm to perform
GaussSeidel iterations with a reduced decision diagram traversal overhead
(a cost also encountered by Kroneckerbased approaches).
Then, we show how even better speedup can be achieved through a caching scheme.
The complexity of our algorithm is linear in the number of nonzero entries
in the transition rate matrix, and, even more importantly, it is independent
of the number L of submodels in which the CTMC is decomposed under
most common conditions.
This is an improvement over previous structured methods, which are
plagued by this L factor in practice.
The advantages of our algorithm are supported by experimental results and a
comparison with the tool PRISM.
X. Jin, G. Ciardo, T.H. Kim, and Y. Zhao.
Symbolic verification and test generation for a network
of communicating FSMs.
In Proc. ATVA,
LNCS 6996, pages 432442.
2011.

We apply the saturation heuristic to the bisimulation problem for
deterministic discreteevent models, obtaining
the fastest to date symbolic bisimulation algorithm, able to deal
with large quotient spaces.
We compare performance of our algorithm with that of Wimmer et al.,
on a collection of models.
As the number of equivalence classes increases, our algorithm tends to have
improved time and space consumption compared with the algorithm
of Wimmer et al., while, for some models with fixed numbers of state variables,
our algorithm merely produced a moderate extension of the number of classes
that could be processed before succumbing to statespace explosion.
We conclude that it may be possible to solve the bisimulation problem
for systems having only visible deterministic transitions
(e.g., Petri nets where each transition has a distinct label)
even if the quotient space is large (e.g., 10^9 classes),
as long as there is strong event locality.
M. Mumme and G. Ciardo.
A fully symbolic bisimulation algorithm.
In Proc. Reachability Problems,
LNCS 6945, pages 218230.
2011.

We apply the saturation heuristic to the bisimulation problem for
deterministic discreteevent models, obtaining
the fastest to date symbolic bisimulation algorithm, able to deal
with large quotient spaces.
We compare performance of our algorithm with that of Wimmer et al.,
on a collection of models.
As the number of equivalence classes increases, our algorithm tends to have
improved time and space consumption compared with the algorithm
of Wimmer et al., while, for some models with fixed numbers of state variables,
our algorithm merely produced a moderate extension of the number of classes
that could be processed before succumbing to statespace explosion.
We conclude that it may be possible to solve the bisimulation problem
for systems having only visible deterministic transitions
(e.g., Petri nets where each transition has a distinct label)
even if the quotient space is large (e.g., 10^9 classes),
as long as there is strong event locality.
Y. Zhao, X. Jin, and G. Ciardo.
A symbolic algorithm for shortest EG witness generation.
In Proc. TASE,
pages 6875.
2011.

Witness generation is a fundamental model checker feature, but
generating shortest witnesses for an EG CTL formula has long been
an open problem of both theoretical and practical relevance.
We propose a symbolic approach to shortest EG witness generation
based on edgevalued multiway decision diagrams.
We employ a fixpoint symbolic iteration to compute the transitive
closure enhanced with distance information, using
the saturation algorithm to cope with the high computational
complexity of this approach.
We also extend this approach to tackling the shortest witness generation
for other properties and the shortest fair witness generation.
Experimental results show that our approach can generate a shortest
witness which could not be found within acceptable time using previous
algorithms.
Y. Zhao and G. Ciardo.
Symbolic computation of strongly connected components using saturation.
In Proc. 2nd NASA Formal Methods Symposium (NFM 2010),
NASA/CP2010216215,
pages 201211.
Apr. 2010.

Finding strongly connected components (SCCs) in the statespace of
discretestate models is a critical task in formal verification of
LTL and fair CTL properties, but the potentially huge number of reachable
states and SCCs constitutes a formidable challenge.
This paper is concerned with computing the sets of states in SCCs or
terminal SCCs of asynchronous systems.
Because of its advantages in many applications, we employ
saturation on two previously proposed approaches:
the XieBeerel algorithm and transitive closure.
First, saturation speeds up statespace exploration when computing each SCC in the XieBeerel algorithm.
Then, our main contribution is a novel algorithm to compute the transitive
closure using saturation.
Experimental results indicate that our improved algorithms
achieve a clear speedup over previous algorithms in some cases.
With the help of the new transitive closure computation algorithm,
up to 10^150 SCCs can be explored within a few seconds.
Y. Zhao and G. Ciardo.
Symbolic CTL model checking of asynchronous systems using constrained
saturation.
In Proc. 7th International Symposium on Automated Technology
for Verification and Analysis (ATVA),
LNCS 5799,
pages 368381.
Macao, China,
Oct. 2009.

The saturation statespace generation algorithm has demonstrated clear
improvements over stateoftheart symbolic methods for asynchronous systems.
This work is motivated by efficiently applying saturation to CTL model checking.
First, we introduce a new ``constrained saturation'' algorithm which constrains
state exploration to a set of states satisfying given properties.
This algorithm avoids the expensive afterthefact intersection operations
and retains the advantages of saturation, namely, exploiting event locality
and benefiting from recursive local fixpoint computations.
Then, we employ constrained saturation to build the set of states satisfying
EU and EG properties for asynchronous systems.
The new algorithm can achieve ordersofmagnitude reduction in runtime
and memory consumption with respect to methods based on
breathfirst search, and even with a previouslyproposed hybrid approach
that alternates between ``safe'' saturation and ``unsafe'' breadthfirst
searches.
Furthermore, the new approch is fully general, as it does
not require the nextstate function to be expressable in Kronecker form.
We conclude this paper with a discussion of some possible future work,
such as building the set of states belonging to strongly connected components.
G. Ciardo, G. Mecham, E. PaviotAdet, and M. Wan.
Psemiflow computation with decision diagrams.
In Proc. 30th International Conference on
Application and Theory
of Petri nets and Other Models of Concurrency (ICATPN),
LNCS 5606,
pages 143162,
Paris, France,
June 2009.

We present a symbolic method for psemiflow computation,
based on zerosuppressed decision diagrams.
Both the traditional explicit methods and our new symbolic method rely on
Farkas' algorithm, and compute a generator set from which any psemiflow
for the Petri net can be derived through a linear combination.
We demonstrate the effectiveness of four variants of our algorithm by applying
them on a suite of Petri net models, showing that our symbolic approach
can produce results in cases where the explicit approach is infeasible.
M. Wan and G. Ciardo.
Symbolic reachability analysis of integer timed Petri nets.
In Proc. 35th International Conference on
Current Trends in Theory and Practice of
Computer Science (SOFSEM), pages 595608,
Spindleruv Mlyn, Czech Republic,
February 2009.

Petri nets are an effective formalism to model discrete event
systems, and several variants have been defined to explicitly
include real time in the model.
We consider two fundamental reachability problems for Timed Petri Nets
with positive integer firing times:
timed reachability (find all markings where the model
can be at a given finite time) and earliest reachability
(find the minimum time when each reachable marking is entered).
For these two problems, we define efficient symbolic algorithms that make use
of both ordinary and edgevalued decision diagrams, and provide
runtime results on an extensive suite of models.
M. Wan and G. Ciardo.
Symbolic statespace generation of asynchronous systems using
extensible decision diagrams.
In Proc. 35th International Conference on
Current Trends in Theory and Practice of
Computer Science (SOFSEM), pages 582594,
Spindleruv Mlyn, Czech Republic,
February 2009.

We propose a new type of canonical decision diagrams,
which allows a more efficient symbolic statespace generation
for general asynchronous systems by allowing onthefly extension of
the possible state variable domains.
After implementing both breadthfirst and saturationbased statespace
generation with this new data structure in our tool SMART,
we are able to exhibit substantial efficiency improvements with respect
to traditional "static" decision diagrams.
Since our previous works demonstrated that saturation
outperforms breadthfirst approaches,
saturation with this new structure is now arguably the
stateoftheart algorithm for symbolic statespace generation
of asynchronous systems.
K. Trivedi, G. Ciardo, B. Dasarathy, M. Grottke, M. Rivalino, A. Rindos, and
B. Varshaw.
Achieving and assuring high availability.
In Proc. 5th International Service Availability Symposium (ISAS),
pages 2025,
Tokyo, Japan,
May 2008.

We discuss availability aspects of large softwarebased systems.
We classify faults into Bohrbugs, Mandelbugs and agingrelated bugs, and then
examine mitigation methods for the last two bug types.
We also consider quantitative approaches to availability assurance.
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),
LNCS 4424,
pages 648663.
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
Multiway Decision Diagrams (MDDs).
This is based on the established Saturation
algorithm which benefits from a nonstandard search strategy that is
very different from breadthfirst search. To bound Saturation, we
employ EdgeValued MDDs and rework its search strategy.
Experimental results show that our algorithm often, but not always,
compares favorably against two SATbased 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 121136.
Berlin, Germany,
July 2007.

The Saturation algorithm for symbolic statespace generation
is a recent advance in exhaustive verification of complex systems,
in particular globallyasynchronous/ locallysynchronous 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
statespace 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 largescale 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 statespace generators.
In Proc. Computer Aided Verification (CAV),
LNCS 4590,
pages 268280.
Berlin, Germany,
July 2007.

Symbolic statespace 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
statespace generator on a sharedmemory 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 dualprocessor, dualcore PC show that
Cilk can improve the runtime 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),
LNCS 4546,
pages 83103.
Siedlce, Poland,
June 2007.

Choosing a good variable order is crucial for making symbolic
statespace generation algorithms truly efficient. One such
algorithm is the MDDbased 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 decisiondiagram 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 timeefficiency and memoryefficiency, as
we demonstrate by extensive benchmarking.
M.Y. Chung, G. Ciardo, and A. J. Yu.
A finegrained fullnessguided chaining heuristic
for symbolic reachability analysis.
In Proc. 4th International Symposium on Automated Technology
for Verification and Analysis (ATVA),
LNCS 4218,
pages 5166.
Beijing, China,
Oct. 2006.

Chaining can reduce the
number of iterations required for symbolic statespace generation and
modelchecking, especially in Petri nets and similar asynchronous systems,
but requires considerable insight and is limited to a static
ordering of the events in the highlevel model.
We introduce a twostep approach that is instead
finegrained 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 breadthfirst and
saturation statespace 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),
LNCS 3920,
pages 90104.
Vienna, Austria,
March 2006.

We investigate a new class of metrics to find good
variable orders for decision diagrams in symbolic statespace
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 statespace 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 statespace generation algorithms: classic
breadthfirst 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 statespace generation.
In Proc. International Parallel and Distributed Processing Symposium
(IPDPS),
Rodos, Greece, April 2006.

The saturation strategy
for symbolic statespace generation is very effective for globallyasynchronous
locallysynchronous discretestate 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.
Saturationbased symbolic reachability analysis
using conjunctive and disjunctive partitioning.
In Proc. Correct Hardware Design and Verification Methods (CHARME) ,
LNCS 3725,
pages 146161.
Saarbrucken, Germany,
Oct. 2005.

We propose a new saturationbased
symbolic statespace generation algorithm for finite discretestate systems.
Based on the structure of the highlevel 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 fixedpoint image
computation strategy completely different from the standard breadthfirst
approach employing a global fixpoint image computation.
Compared to breadthfirst 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 runtimes and peak memory
than previous saturation algorithms.
G. Ciardo.
Implicit representations and algorithms
for the logic and stochastic analysis of discretestate systems
In Proc. Formal Techniques for Computer Systems and Business Processes ,
LNCS 3670,
pages 1517.
Paris, France,
Sept. 2005.

(Invited Keynote Paper)
M.Y. Chung and G. Ciardo.
A pattern recognition approach for speculative firing prediction
in distributed saturation statespace generation.
In Proc. Workshop on Parallel and Distributed Model Checking (PDMC) ,
pages 6579.
Lisbon, Portugal,
July 2005.

The saturation strategy for symbolic statespace generation is particularly
effective for globallyasynchronous locallysynchronous 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 historybased 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 discretestate techniques and mitigate the impact of the resulting statespace 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 realworld 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 272281.
Enschede, The Netherlands,
Sept. 2004.

We present a distributed version of the saturation algorithm
for symbolic statespace generation of discretestate models.
The execution is strictly sequential but utilizes the overall available memory.
Thanks to a levelbased 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,
LNCS 3099,
pages 1734.
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 Multivalued 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.
Profitdriven service differentiation in transient environments.
In
Proc. 11th IEEE/ACM Int. Symposium on Modeling, Analysis
and Simulation of Computer and Telecommunication Systems (MASCOTS),
pages 230233.
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 discreteevent simulation through structural caching.
In
Proc. Sixth Int. Workshop on Performability
Modeling of Computer and Communication Systems (PMCCS6),
pages 1114.
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 highlevel 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 (PMCCS6),
pages 2326.
Urbana, IL, USA,
Sept. 2003.

We present a regenerative simulation method applicable to a
special class of nonMarkovian 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 phasetype firing delays in both discrete and continuous
time simultaneously in the same model.
However, exact numerical analysis requires that the discretetime
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. S. Miner.
Comparing implicit representations of large CTMCs.
In Numerical Solution of Markov Chains,
pages 323327.
Urbana, IL, USA,
Sept. 2003.

Highlevel formalisms of stochastic structures can express very
large continuoustime Markov chains (CTMC).
State explosion poses interesting challenges in terms of data structures
and numerical solution algorithms.
Implicit representations exploit structural properties of the highlevel
model, to avoid storing each nonzero matrix entry explicitly.
Implicit structures used to store the CTMC include Kronecker algebra,
multiterminal 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 indepth comparison of implicit CTMC techniques,
we present some initial observations and
discuss the currentlyknown 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 7897.
UrbanaChampaign, IL, USA,
Sept. 2003.
SpringerVerlag.

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
statespace generation techniques, as well as symbolic CTL modelchecking
algorithms, are available.
For the study of stochastic and timing behavior, both
sparsestorage and Kronecker numerical solution approaches are available
when the underlying process is a Markov chain.
In addition, discreteevent simulation is always applicable regardless
of the stochastic nature of the process, but
certain classes of nonMarkov 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 4053.
Boulder, CO, USA,
July 2003.
SpringerVerlag.

In previous work, we showed how structural information can be used to
efficiently generate the statespace 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 fixedpoint iteration strategies,
resulting in ordersofmagnitude reductions for both execution times and
memory consumption in comparison to wellestablished 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 379393.
Warsaw, Poland,
Apr. 2003.
SpringerVerlag.

In previous work, we proposed a ``saturation'' algorithm
for symbolic statespace generation characterized by the use of
multivalued decision diagrams, boolean Kronecker operators,
event locality, and a special iteration strategy.
This approach outperforms traditional BDDbased 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 statespace discovery with symbolic global statespace generation.
This relieves the modeler from worrying about the behavior of submodels
in isolation.
G. Ciardo and R. Siminiceanu.
Using edgevalued decision diagrams for symbolic generation of shortest paths.
In Proceedings of the Fourth International Conference on Formal Methods
in ComputerAided Design (FMCAD),
LNCS 2517,
pages 256273.
Portland, OR, USA,
Nov. 2002.
SpringerVerlag.

We present a new method for the symbolic construction of
shortest paths in reachability graphs.
Our algorithm relies on a variant of edgevalued decision diagrams
that supports efficient fixedpoint 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 104111.
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 onthefly, 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 316.
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 discretestate systems.
However, their practical applicability is limited by the statespace
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 statetostate 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 165174.
Aachen, Germany,
Sept. 2001.
IEEE Comp. Soc. Press.

We present a novel stochastic Petri net formalism where both discrete and
continuous phasetype firing delays can appear simultaneously
in the same model.
By capturing nonMarkovian behavior in discrete or continuous time,
as appropriate, the formalism affords higher modeling fidelity.
Alone, discrete or continuous phasetype Petri nets have simple underlying
Markov chains, but mixing the two complicates matters.
We show that, in a mixed model where discretetime transitions are synchronized,
the underlying process is semiregenerative and we can employ Markov renewal
theory to formulate stationary or timedependent solutions.
Also noteworthy are the computational tradeoffs between the
socalled 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 114123.
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 recentlyproposed and very popular
GreedyDualSize (GDS) policy is based on document size and has an
elegant aging mechanism. Similarly, the GreedyDualFrequency (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 GDSlike
replacement policies emphasizing size yield the best file
hit ratio but typically show poor byte hit ratio, while
GDFlike replacement policies emphasizing frequency have better
byte hit ratio but result in worse file hit ratio. In this paper, we
propose a generalization of GreedyDualFrequencySize 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 statespace generation.
In Proc. Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2001),
pages 328342.
Genova, Italy,
Apr. 2001.
SpringerVerlag.

We present a novel algorithm for generating state spaces of
asynchronous systems using Multivalued Decision Diagrams. In
contrast to related work, we encode the nextstate function of a
system not as a single Boolean function, but as crossproducts 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 BDDbased statespace
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 434441.
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: longterm popularity and
shortterm 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 shortterm 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 heavytailed distributions.
In Proceedings of the Workshop on Software Performance Analysis (WOSP),
pages 147157.
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 multiserver 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 statespace 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 103122.
June 2000.
SpringerVerlag.

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
Multivalued 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 runtime results show that it often performs
significantly faster than existing statespace generators.
A. S. 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 207216.
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 productform 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. S. Miner.
Structural approaches for SPN analysis.
In A. Tenter, editor,
High Performance Computing 2000, Grand Challenges in
Computer Simulation,
pages 345356.
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 stateoftheart 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 aggregationbased solution method for M/G/1type processes.
In W. Stewart and B. Plateau, editors,
Numerical Solution of Markov Chains, pages 2140, Sept. 1999.
Prensas Universitarias de Zaragoza.

We extend the ETAQA approach, initially proposed
for the efficient numerical solution of a class of
quasi birthdeath processes,
to the more complex case of M/G/1type Markov processes.
The proposed technique can be used for the exact
solution of a class of M/G/1type 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. S. 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 2231.
Sept. 1999.
IEEE Comp. Soc. Press.

Kroneckerbased 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. S. 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 625.
June 1999.
SpringerVerlag.

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 Multivalued 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
birthdeath processes.
In
Proceedings of the Fourth International Workshop on Performability
Modeling of Computer and Communication Systems (PMCCS4) ,
pages 5861.
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
twodimensional generalizations of elementary M/G/1 and
G/M/1 queues [Kleinrock, 1975].
The intersection of these two
cases corresponds to the socalled quasibirthdeath (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 faulttolerant jointheshortestqueue policy.
In
Proceedings of the Fourth International Workshop on Performability
Modeling of Computer and Communication Systems (PMCCS4),
pages 3438.
Williamsburg, VA, USA,
Sept. 1998.

In distributed or multiprocessor 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 matrixgeometric 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 3443.
Durham, NC, USA,
Sept. 1998.
IEEE Computer Society Press.

Transient analysis of nonMarkovian 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 finitecapacity 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/GIFachtagung: Messung, Modellierung und
Bewertung von Rechen und Kommunikationssystemen (MMB'97),
(Measurement, Modeling, and Valuation of Computer and CommunicationSystems),
pages 103117.
Freiberg, Germany,
Sept. 1997.
VDEVerlag.

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 timeextended
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 nonexponentially
distributed timing is still one of the major problems for the
analysis and was first attacked for continuoustime 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
discretetime 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 discretetime models.
G. Ciardo, D. Nicol, K. Trivedi.
Discreteevent simulation of fluid stochastic Petri nets.
In Proc. Int. Workshop on Petri Nets and Performance Models (PNPM'97),
pages 217225.
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 4457.
St. Malo, France,
June 1997.
SpringerVerlag.

We consider the problem of storing and searching a large
state space obtained from a highlevel 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, UrbanaChampaign, 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 discretetime Markov chains.
Mixedtime nonMarkovian models can be studied
using simulation.
Multiple interacting models and
fixedpoint 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 215234.
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 steadystate and transient solutions
are possible, to compute the specified ratebased and
impulsebased 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.
Advances in compositional approaches based on Kronecker algebra:
Application to the study of manufacturing systems
In
Proceedings of the Third International Workshop on Performability
Modeling of Computer and Communication Systems (PMCCS3) ,
pages 6165.
Bloomingdale, IL, USA,
Sept. 1996.

Recent developments in the use of Kronecker algebra for the solution of
continuoustime Markov chains (CTMCs),
in particular models based on
stochastic Petri nets, have increased the size of the systems that can be
analyzed using exact numerical methods.
We report on the more recent results, and employ them
to study a kanban system.
G. Ciardo and R. Zijal.
Welldefined stochastic Petri nets.
In Proc. 4th Int. Workshop on Modeling, Analysis and Simulation
of Computer and Telecommunication Systems (MASCOTS'96),
pages 278284.
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 statedependent impulse
reward measures.
We propose a definition of welldefined SPNs, which takes into account
whether the basic underlying stochastic process or the derived reward
processes are determined. A statespacebased
algorithm to determine whether a given SPN is welldefined is provided.
G. Ciardo, L. Cherkasova, V. Kotov, and T. Rokicki.
Modeling a scalable highspeed interconnect with stochastic Petri nets.
In Proc. Int. Workshop on Petri Nets and Performance Models
(PNPM'95),
pages 8392.
Durham, NC,
Oct. 1995,
IEEE Comp. Soc. Press.

This paper presents an approach to using Stochastic Petri nets to
model largescale 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 319320.
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
steadystate performance of the system.
Discreteevent 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.
Discretetime Markovian stochastic Petri nets.
In W. J. Stewart, editor, Computations with Markov Chains,
pages 339358.
Raleigh, NC,
Jan. 1995.
Kluwer.

We revisit and extend the original definition of discretetime 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
discretetime 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 wellknown 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 144157.
SophiaAntipolis, France,
June 1994.
SpringerVerlag.

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 markingdependent 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 179198.
Zaragoza, Spain
June 1994.
SpringerVerlag,

We discuss P/Tnets where the
arc cardinalities are allowed to be markingdependent 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 psemiflows of a P/Tnet with markingdependent arc cardinality
can be obtained from the psemiflows of a related ordinary P/Tnet
and how bounds on the relative throughputs of the transitions can be obtained,
a weaker condition than tsemiflows.
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 170179.
Toulouse, France,
Oct. 1993.
IEEE Comp. Soc. Press.

Stochastic Petri nets (SPNs) with generally distributed firing times
are isomorphic to generalized semiMarkov 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),
semiMarkovian stochastic Petri nets (SMSPNs),
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 continuoustime
case (PHtype 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 160169.
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.
Closedform 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 576581.
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 markingdependent
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 367372.
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 565595.
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 errorprone 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 fixedpoint 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
fixedpoint 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 7483.
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 142151.
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 markingdependent 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 steadystate and transient solvers are available;
cumulative and uptoabsorption 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 SPNbased 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 5462.
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 8492.
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 faulttolerant multiple processor systems.
In N. A. E. Ata, editor, Modelling Techniques and Tools for
Performance Analysis '85. Elsevier Science Publishers B.V.
(NorthHolland), 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 613.
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 155170.
INRIA, Elsevier Science Publishers B.V. (NorthHolland), June 1985.
G. Ciardo and C. Iacobelli.
On the relationalCODASYL 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 707712.
Gaithersburg, Maryland,
May 1984.
IEEE and NBS.
Book Chapters
R. Siminiceanu and G. Ciardo.
Symbolic model checking for avionics.
In S. Gnesi and T. Margaria, editors,
Formal Methods for Industrial Critical Systems: A Survey of Applications,
pages 85112,
Wiley, 2012.

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 371394.
SpringerVerlag, 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 crossproduct 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 discretestate models.
In particular, we discuss both explicit and symbolic algorithms
for statespace generation, CTL modelchecking,
and continuoustime 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 344374.
SpringerVerlag, 2001.

Both the logic and the stochastic analysis of discretestate
systems are hindered by the combinatorial growth of the state space
underlying a highlevel model.
In this work, we consider two orthogonal approaches to cope with
this ``statespace 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 1141.
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 continuoustime MCs (CTMCs),
but we occasionally refer to discretetime 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, Stateofthe
Art in Performance Modeling and Simulation: Advanced Computer Systems,
pages 203234.
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 semiMarkov or Markovregenerative.
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 587612.
SpringerVerlag, 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. Continuoustime Markov chains (CTMCs)
are compared with (continuoustime) Markov reward models (MRMs)
and generalized stochastic Petri nets (GSPNs) are compared
with stochastic reward nets (SRNs).
It is shown that rewardbased
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 nonexponentiality, 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 145191.
SpringerVerlag, 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 (timeindependent) 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. NorthHolland, 1985.
Theses, Tutorials, Reports, etc.
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 Modelchecking 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):913914, 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 ComputerCommunication Systems,
pages 2934.
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
statespace 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 4143.
Saint Malo, France,
June 1997.

SMART is a new tool designed to allow various highlevel 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):601602, 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.
DagstuhlSeminarReport 115  22.05.26.05.95 (9521).
K. Trivedi, A. Bobbio, G. Ciardo, R. German, A. Puliafito, and M. Telek.
NonMarkovian Petri nets.
In Proc. 1995 ACM SIGMETRICS Conf. on Measurement and Modeling
of Computer Systems,
pages 263264.
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 390391.
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):97100, 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.
Last updated: January 28, 2014.
Report suggestions and problems to:
ciardo@iastate.edu