Behavioural equivalences for fluid stochastic Petri nets

TL;DR

This paper introduces fluid equivalences for labeled fluid stochastic Petri nets, enabling behavior comparison and reduction while preserving key properties, with applications in performance analysis and logical characterization.

Contribution

It defines fluid trace and bisimulation equivalences, proves their preservation of performance measures, and introduces novel fluid modal logics for behavioral characterization.

Findings

Fluid trace equivalence preserves average fluid change volume.

Fluid bisimulation equivalence preserves stationary probabilities and fluid distributions.

Quotienting by fluid bisimulation simplifies analysis of LFSPNs.

Abstract

We propose fluid equivalences to compare and reduce behaviour of labeled fluid stochastic Petri nets (LFSPNs) while preserving their discrete and continuous properties. We define a linear-time relation of fluid trace equivalence and its branching-time counterpart, fluid bisimulation equivalence. Both fluid relations take into account the essential features of the LFSPNs behaviour: functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose continuous markings have no influence to the discrete ones and whose discrete part is continuous time stochastic Petri nets. The underlying stochastic model for the discrete part of the LFSPNs is continuous time Markov chains (CTMCs). The performance analysis of the continuous part of LFSPNs is accomplished via the associated stochastic fluid models (SFMs). We show that fluid trace equivalence preserves average potential fluid change volume for the transition sequences of every certain length. We prove that fluid bisimulation equivalence preserves the aggregated probability functions: stationary probability mass for the underlying CTMC, as well as stationary fluid buffer empty probability, fluid density and distribution for the associated SFM. Hence, the equivalence guarantees identity of a number of discrete and continuous performance measures. Fluid bisimulation equivalence is then used to simplify the qualitative and quantitative analysis of LFSPNs via quotienting the discrete reachability graph and underlying CTMC. To describe the quotient associated SFM, the quotients of the probability functions are defined. We characterize logically fluid trace and bisimulation equivalences with two novel fluid modal logics $HML_{flt}$ and $HML_{flb}$, based on the Hennessy-Milner Logic HML. The application example of a document preparation system demonstrates the behavioural analysis via quotienting by fluid bisimulation equivalence.

Tables

Table 1. Table 1: Abbreviations used in the paper

Petri nets		Markov chains
SPN	stochastic Petri net	CTMC	continuous time
CTSPN	continuous time stochastic Petri net		Markov chain
GSPN	generalized stochastic Petri net	SMC	semi-Markov chain
FSPN	fluid stochastic Petri net	Fluid models
LFSPN	labeled fluid stochastic Petri net	SFM	stochastic fluid model
Probability functions		Rate matrices
PMF	probability mass function	TRM	transition rate matrix
PDF	probability distribution function	FRM	fluid rate matrix

Table 2. Table 2: Behavioural aspects of LFSPNs in the logical modalities and interpretations

Fluid	Semantics type	Functional activity	Stochastic timing	Fluid flow
modal logic	(linear/branching time)	(action occurrences)	(transition rates)	(fluid rates)
$HM{L}_{flt}$	$\top$	$⟨a⟩$	${[[\cdot ]]}_{flt}(M,\varsigma ,\varrho )$ (by $\varsigma$)	${[[\cdot ]]}_{flt}(M,\varsigma ,\varrho )$ (by $\varrho$)
$HM{L}_{flb}$	$\top$, $\neg$, $\wedge$	${\nabla }_a$, ${⟨a⟩}_{\lambda }$ (by $a$)	${⟨a⟩}_{\lambda }$ (by $\lambda$)	${\wr }_r$

Equations

$$RE(M)=\sum _{t\in Ena(M)}{\Omega }_N(t,M).$$

$$SJ(M)=\frac{1}{{\sum }_{t\in Ena(M)}{\Omega }_N(t,M)}=\frac{1}{RE(M)}.$$

$$VAR(M)=\frac{1}{{\left({\sum }_{t\in Ena(M)}{\Omega }_N(t,M)\right)}^2}=\frac{1}{RE(M{)}^2}.$$

$$RM(M,\tilde{M})=\sum _{\{t\mid M\stackrel{t}{\to }\tilde{M}\}}{\Omega }_N(t,M).$$

$${\cal Q}_{ij}=\left\{\begin{array}[]{ll}RM(M_{i},M_{j}),&i\neq j;\\ -\sum_{\{k\mid 1\leq k\leq n,\ k\neq i\}}RM(M_{i},M_{k}),&i=j.\end{array}\right.$$

$$\phi (\delta )=\phi (0)e^{\mathbf{Q}\delta },$$

$$\varphi_{i}(0)=\left\{\begin{array}[]{ll}1,&M_{i}=M_{N};\\ 0,&\mbox{otherwise}.\end{array}\right.$$

$$\left\{\begin{array}[]{l}\varphi{\bf Q}={\bf 0}\\ \varphi{\bf 1}^{T}=1\end{array}\right.,$$

$$TimeFract(S)=\sum _{\{i\mid M_i\in S\}}{\phi }_i.$$

$$Tokens(p,k)=\sum _{\{i\mid M_i(p)=k,M_i\in DRS(N)\}}{\phi }_i.$$

$$Prob(\mathcal{A})=\sum _{\{i\mid M_i\in DR{S}_{\mathcal{A}}(N)\}}{\phi }_i.$$

$$TokensNum(p)=\sum _{k\ge 1}Tokens(p,k)\cdot k=\sum _{\{i\mid M_i(p)\ge 1,M_i\in DRS(N)\}}{\phi }_i{M}_i(p).$$

$$FiringFreq(t)=\sum _{\{i\mid t\in Ena(M_i),M_i\in DRS(N)\}}{\phi }_i{\Omega }_N(t,M_i).$$

$$ExitFreq(M_i)={\phi }_{i}RE(M_i)=\frac{{\phi }_i}{SJ(M_i)}.$$

$$Prob(r)=\sum _{\{i\mid M_i\in DRS(N)\}}{\phi }_i{r}_i.$$

$$TravFreq(M_i,M_j)={\phi }_{i}RM(M_i,M_j).$$

$$Delay=\frac{TravTokens}{Rate}.$$

$$RP(M(\delta ))=\sum _{\{t\in Ena(M(\delta ))\mid (t,q)\in C_N\}}{R}_N((t,q),M(\delta ))-\sum _{\{t\in Ena(M(\delta ))\mid (q,t)\in C_N\}}{R}_N((q,t),M(\delta )).$$

$$RA(M(\delta),X(\delta))=\frac{dX(\delta)}{d\delta}=\left\{\begin{array}[]{ll}\max\{RP(M(\delta)),0\},&X(\delta)=0;\\ RP(M(\delta)),&(X(\delta)>0)\wedge(RP(M(\delta^{-}))RP(M(\delta^{+}))\geq 0);\\ 0,&(X(\delta)>0)\wedge(RP(M(\delta^{-}))RP(M(\delta^{+}))<0).\end{array}\right.$$

$${\cal R}_{ij}=\left\{\begin{array}[]{ll}RP(M_{i}),&i=j;\\ 0,&i\neq j.\end{array}\right.$$

$$\ell_{i}(0)=\left\{\begin{array}[]{ll}1,&M_{i}=M_{N};\\ 0,&\mbox{otherwise};\end{array}\right.$$

$$F_{i}(0,x)=\left\{\begin{array}[]{ll}1,&(M_{i}=M_{N})\wedge(x\geq 0);\\ 0,&\mbox{otherwise};\end{array}\right.$$

$$f_i(0,x)=0\forall (M_i,x)\in RS(N).$$

$$\ell (\delta )+{\int }_{0+}^{\infty }f(\delta ,x)dx=\phi (\delta ).$$

$$\frac{\partial F(\delta ,x)}{\partial \delta }+\frac{\partial F(\delta ,x)}{\partial x}\mathbf{R}=F(\delta ,x)\mathbf{Q},x>0;$$

$$\frac{\partial f(\delta ,x)}{\partial \delta }+\frac{\partial f(\delta ,x)}{\partial x}\mathbf{R}=f(\delta ,x)\mathbf{Q},x>0.$$

$$\frac{d\ell (\delta )}{d\delta }+f(\delta ,0)\mathbf{R}=\ell (\delta )\mathbf{Q}.$$

$$\ell (\delta )1^T+{\int }_{0+}^{\infty }f(\delta ,x)dx{1}^T=1,$$

$$FluidFlow(q)=\sum _{i=1}^n{\phi }_{i}RP(M_i)=\phi \mathbf{R}{1}^T<0,$$

$$\ell +{\int }_{0+}^{\infty }f(x)dx=\phi .$$

Full text

We show that fluid trace equivalence preserves average potential fluid change volume for the transition sequences of every certain length. We prove that fluid bisimulation equivalence preserves the following aggregated (by such a bisimulation) probability functions: stationary probability mass for the underlying CTMC, as well as stationary fluid buffer empty probability, fluid density and distribution for the associated SFM. Hence, the equivalence guarantees identity of a number of discrete and continuous performance measures. Fluid bisimulation equivalence is then used to simplify the qualitative and quantitative analysis of LFSPNs that is accomplished by means of quotienting (by the equivalence) the discrete reachability graph and underlying CTMC. To describe the quotient associated SFM, the quotients of the probability functions are defined. We also characterize logically fluid trace and bisimulation equivalences with two novel fluid modal logics $HML_{flt}$ and $HML_{flb}$, constructed on the basis of the well-known Hennessy-Milner Logic HML. These results can be seen as operational characterizations of the corresponding logical equivalences. The application example of a document preparation system demonstrates the behavioural analysis via quotienting by fluid bisimulation equivalence.

Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid model, transient and stationary behaviour, probability mass, buffer empty probability, fluid density and distribution, performance analysis, Markovian trace and bisimulation equivalences, fluid trace and bisimulation equivalences, quotient, fluid modal logic, logical and operational characterizations, application example.

1 Introduction

An important scientific problem that has been often addressed in the last decades is the design and analysis of parallel systems, which takes into account both qualitative (functional) and quantitative (timed, probabilistic, stochastic) features of their behaviour. The main goal of the research on this topic is the development of models and methods respecting performance requirements to concurrent and distributed systems with time constraints (such as deterministic, nondeterministic and stochastic time delays) to construct, validate and optimize the performability of realistic large-scale applications: computing systems, networks and software, controllers for industrial devices, manufacturing lines, vehicle, aircraft and transportation engines. A fruitful approach to achieving progress in this direction appeared to be a combined application of the theories of Petri nets, stochastic processes and fluid flow systems to the specification and analysis of such time-dependent systems with inherent behavioural randomicity [51].

1.1 Fluid stochastic Petri nets

In the past, many extensions of stochastic Petri nets (SPNs) [65, 63, 64, 61, 62, 14, 15] have been developed to specify, model, simulate and analyze some particular classes of systems, such as computer systems, communication networks or manufacturing plants. These new formalisms have been constructed as a response to the needs for more expressive power in describing real-world systems, and to the requirements for compact models and efficient analysis techniques. One of the extensions are fluid stochastic Petri nets (FSPNs), capable of modeling hybrid systems that combine continuous state variables, corresponding to the fluid levels, with discrete state variables, specifying the token numbers. The continuous part of the FSPNs allows one to represent the fluid level in continuous places and fluid flow along continuous arcs. This part can naturally describe continuous variables in physical systems whose behaviour is commonly represented by differential equations. Continuous variables may also be used to describe a macroscopic view of discrete items that appear in large populations, e.g., packets in a computer network, molecules in a chemical reaction or people in a crowd. The discrete part of an FSPN is essentially its underlying SPN, obtained from the FSPN by removing all the fluid-related continuous elements. This part usually models the discrete control of the continuous process. The control may demonstrate some stochastic behavior that captures uncertainty about the detailed system behavior.

FSPNs have been proposed in [76, 35, 84] to model stochastic fluid flow systems [50, 46]. To analyze FSPNs, simulation, numerical and matrix-geometric methods are widely used [55, 36, 24, 47, 48, 43, 44, 56, 49]. The major problem of FSPNs is the high complexity of computing their solution, resulting in huge memory and time requirements while analyzing of realistic models. A positive feature of the FSPN formalism is that it hides from a modeler the technical difficulties with solving differential equations for the underlying stochastic processes and that it unifies in one framework the evolution equations for the discrete and continuous parts of systems.

1.2 Equivalences on the related models

However, to the best of our knowledge, neither transition labeling nor behavioral equivalences have been proposed so far for FSPNs. In [77, 78, 79], label equivalence and projected label equivalence have been introduced for Fluid Process Algebra (FPA). FPA is a simple sub-algebra of Grouped PEPA (GPEPA) [52], which is itself a conservative extension of Performance Evaluation Process Algebra (PEPA) [54], obtained by adding fluid semantics with an objective to simplify solving the systems of replicated ordinary differential equations. In [77, 79], it has been proved that projected label equivalence induces a fluid lumpable partition and that both label equivalence and projected label equivalence imply semi-isomorphism (stochastic isomorphism), in the context of a special subclass of well-posed models. Nevertheless, the mentioned label equivalences do not respect the action names; hence, they are not behavioral relations.

In [80, 81], the models specified with large ordinary differential equation (ODE) systems have been explored within Fluid Extended Process Algebra (FEPA). The relations of semi-isomorphism, as well as those of ordinary and projected label equivalence have been proposed for the sequential process components, called fluid atoms, such that they can have a multiplicity (the number of their copies in the model specification). In addition to exact fluid lumpability (EFL) from [77, 79] that allows one to aggregate isomorphic processes with the same multiplicities, a new notion of ordinary fluid lumpability (OFL) has been proposed. OFL does not require that the multiplicities of the isomorphic processes coincide, but it preserves the sums of the aggregated variables instead. Moreover, the approximate versions ($\epsilon$-variants) of semi-isomorphism, EFL and OFL have been investigated, which abstract from small fluctuations of the parameter values in the processes with close (similar) differential trajectories. This means that the close processes become completely symmetric (aggregative, isomorphic) after small change (perturbation) of their parameters, resulting in the closer differential trajectories. It has been proved that the aggregation error depends linearly in the perturbation intensity. However, as mentioned above, the label equivalences do not respect the names of actions and therefore they are not behavioural equivalences.

In [82], two notions of lumpability for the class of heterogenous systems models specified by nonlinear ODEs have been investigated: exact lumpability (EL) [75] and uniform lumpability (UL), both applied for exact aggregation of the state variables. Unlike the EL transformations through linear mappings (in particular, those induced by a partition of the original state space), UL considers exact symmetries of the equations due to identification of the different variables from one partition block, which have coinciding differential trajectories (solutions) in case of the same initial conditions. This is an extension of the ODE systems reduction technique for the formal language $FPA$ from [77] to arbitrary vector fields. Both the lumpability relations do not take into account the action names and do not refer to behavioural equivalences.

In [57], differential bisimulation for FEPA has been constructed. This relation induces a partition on ODEs corresponding to the FEPA terms. Differential bisimulation is a behavioural equivalence that is an ODE analogue of the probabilistic and stochastic bisimulations. For each partition block, the sum of solutions of its ODEs coincides with the solution of a single aggregate ODE for this block. In the framework of FSPNs, the ODE systems are obtained only when there is exactly one continuous place. In the general case (more than one continuous place), the dynamics of FSPNs is described by the systems of equations with partial derivatives of probability distribution functions (PDFs) and probability density functions with respect to fluid levels in the continuous places. These levels are the random variables with a parameter accounting for the work time of an FSPN, starting from the initial moment. Just for the fluid levels, the ODEs over the time variable can be constructed in each discrete marking. However, the sojourn time in each discrete marking is a random variable, calculated as the minimal transition delay, among all the transitions enabled in the marking. The FEPA processes are described by the ODE systems with derivatives of the population functions that define the multiplicities (numbers of replicas) of fluid atoms by only one variable denoting the time. Thus, the analogues of the FEPA fluid atoms are the (mainly, continuous) places of FSPNs. Hence, the FSPN model always has a naturally embedded notion of population, seen as a fluid in a continuous place. The systems behaviour is treated in FSPNs on a higher level of specification using the continuous time concept and the GSPN basic model, and also on a higher analysis level using the theories of probability and stochastic processes for constructing the underlying SMCs, CTMCs and stochastic fluid models (SFMs). The multiplicities of the FEPA fluid atoms are the functions of time, such that their values can be found for every particular time moment. In contrast, the fluid levels in continuous places of FSPNs are the continuous random variables that depend on time, so that their exact values at a given moment of time cannot be calculated. The reason is the property of the continuous probability distributions, stating that a continuous random variable may be equal to a concrete fixed value with zero probability only (excepting that in FSPNs, the fluid probability mass at the boundaries may be positive). In addition, the FEPA expressivity is rather restricted by considering only the processes, such that each of them is a parallel composition (with embedded synchronization by the cooperation actions) of the fluid atoms denoting a large number of copies of the simple sequential components, specified with only three operations: prefix, choice and recursive definition with constants. Moreover, the fluid atoms in FEPA are considered uniformly, i.e. these is no difference between “discrete” atoms with small multiplicities and “continuous” ones with large multiplicities. However, the tokens in FSPNs are jumped from one discrete place to another instantaneously when their input of output transitions fire, whereas the fluid flow proceeds through continuous places during all the time period when their input or output transitions are enabled. Thus, the notion of differential bisimulation cannot be straightforwardly transferred from FEPA to FSPNs, since the two models are different in many parts.

In [29, 30, 32], back and forth bisimulation equivalences on chemical species have been introduced for chemical reaction networks (CRNs) with the ODE-based semantics. The forth bisimulation induces a partition where each equivalence class is a sum of concentrations of the species from this class, and this relation guarantees the ordinary fluid lumping on the ODEs of CRNs. The back bisimulation relates the species with the same ODE solutions at all time points, starting from the moment for which their equal initial conditions have been defined, and this relation characterizes the exact fluid lumping on the ODEs of CRNs. It has been noticed that the bisimulations proposed in [29] differ from the equivalences from [77, 78, 79, 80, 81], since the former ones relate single variables whereas the latter ones relate the sets of variables, such that each of them represents the behaviour of some sequential process. The CRNs dynamics is described by ODEs with derivatives with respect to one variable (time), and the CRNs behaviour is deterministic, described by differential trajectories. In [32], an algorithm for constructing exact aggregations for a class of ODE systems has been proposed, which computes forward and backward bisimulation equivalences of CRNs with the time complexity $O(rs\log s)$ and space complexity $O(rs)$, where $r$ is the number of monomials and $s$ is the number of variables in the ODEs. As mentioned above, unlike CRNs, FSPNs have a stochastic behaviour which is influenced by the interplay of time and probabilistic factors. The FSPNs dynamics is analyzed with (multidimensional, in general) SFMs that are solved using the differential equations with partial derivatives with respect to several variables. In [74], back bisimulation equivalence, called there back differential equivalence (BDE), has been used to provide an alternative characterization of emulation for CRNs, interpreted as the systems of ODEs. Being a stricter variant of BDE, emulation requires that the ODE solutions of a source CRN exactly overlap those of a target one at all moments of time. A genetic algorithm is presented that uses BDE to discover emulations between CRNs.

In [31], back differential equivalence (BDE) and forth differential equivalence (FDE) have been explored for a basic formalism, called Intermediate Drift Oriented Language (IDOL). IDOL has a syntax to specify drift for a class of non-linear ODEs, for which the decidability results are known. The mentioned equivalence relations can be transferred from IDOL to the higher-level models, such as Petri nets, process algebras and rule systems, interpreted as ODEs. The differential equivalences embrace such notions as minimization of CTMCs based on the lumpability relation [39], bisimulations of CRNs [29] and behavioural relations for process algebras with the ODE semantics [57]. At the same time, the ODE class defined by the IDOL language cannot specify semantics of the systems with stochastic continuous time delays in the discrete states, as well as many other behavioural aspects of FSPNs, including the ones mentioned above. In [33], an application tool ERODE has been presented for solution and reduction of the ODE systems. The tool supports the mentioned BDE and FDE relations over the ODE variables.

In [5], on the product form queueing networks (QNs), the ideas of equivalent flow server and flow equivalence have been applied to the models reduction. This has been done by aggregating server stations and their states by the latter equivalence relation. Nevertheless, flow equivalence does not respect the names of actions, hence, it is not a behavioural equivalence.

In [26], for systems of polynomial ODEs, the questions of reasoning (detecting and proving identities among the variables of an ODE system) and reduction (decreasing and possibly minimizing the number of variables and equations of an ODE system while preserving all important information) have been addressed. The initial value problem has been considered, i.e. solving the ODE systems with initial conditions. The ${\cal L}$-bisimulation equivalence on the polynomials in the variables has been defined, which agrees with the underlying ODEs. An algorithm has been proposed that detects all valid identities in an ODE system. This allows one to construct the reduced ODE system with the minimal number of variables and equations so that the system is equivalent to the initial one. However, ${\cal L}$-bisimulation equivalence does not take into account the names of actions (which are not present at all in the ODE systems specifications), therefore, the equivalence is not a behavioural relation.

1.3 Labeled fluid stochastic Petri nets and fluid equivalences

In this paper, we propose the behavioural relations of fluid trace and bisimulation equivalences that are useful for the comparison and reduction of the behaviour of labeled FSPNs (LFSPNs), since these relations preserve the functionality and performability of their discrete and continuous parts.

For every FSPN, the discrete part of its marking is determined by the natural number of tokens contained in the discrete places. The continuous places of an FSPN are associated with the non-negative real-valued fluid levels that determine the continuous part of the FSPN marking. Thus, FSPNs have a hybrid (discrete-continuous) state space. The discrete part of every hybrid marking of FSPNs is called discrete marking while the continuous part is called continuous marking. The discrete part of each hybrid marking has an influence on the continuous part. For more general FSPNs, the reverse dependence is possible as well. As a basic model for constructing LFSPNs, we consider only those FSPNs in which the continuous parts of markings have no influence on the discrete ones, i.e. such that every discrete part determines completely both the set of enabled transitions and the rates of incoming and outgoing arcs for each continuous place [43, 49]. We also require that the discrete part of LFSPNs should be labeled continuous time stochastic Petri nets (CTSPNs) [63, 61, 62, 14].

First, we define a linear-time relation of fluid trace equivalence on LFSPNs. Linear-time equivalences, unlike branching-time ones, do not respect the points of choice among several alternative continuations of the systems behavior. We require that fluid trace equivalence on discrete markings of two LFSPNs should be a standard (strong) Markovian trace equivalence. Hence, for every sequence of discrete markings and transitions in the discrete reachability graph of an LFSPN, starting from the initial discrete marking and ending in some last discrete marking (such sequence is called path), we require a simulation of the path in the discrete reachability graph of the equivalent LFSPN, such that the action labels of the corresponding fired transitions in the both sequences coincide. Moreover, the average sojourn times in (or the exit rates from) the respective discrete markings should be the same. Finally, for the two equivalent LFSPNs, the cumulative execution probabilities of all the paths corresponding to a particular sequence of actions, together with a concrete sequence of the average sojourn times (exit rates), should be equal. Thus, when comparing the execution probabilities, we parameterize the paths with the same extracted action sequence by all possible sequences of the extracted average sojourn times (exit rates), i.e. we consider comparable only the paths with the same extracted action sequence and the same value of the parameter, which is a concrete sequence of the extracted average sojourn times (exit rates). Therefore, our definition of the trace equivalence on the discrete markings of LFSPNs is similar to that of ordinary (that with the absolute time counter or with the countdown timer) Markovian trace equivalence [83] on transition-labeled CTMCs. Ordinary Markovian trace equivalence and its variants from [83] have been later investigated and enhanced on sequential and concurrent Markovian process calculi SMPC and CMPC in [18, 16, 17, 19] and on Uniform Labeled Transition Systems (ULTraS) in [20, 21].

As for the continuous markings of the two LFSPNs, we further parameterize the paths with the same extracted action sequence and the same sequence of the extracted average sojourn times (exit rates) by counting the execution probabilities only of those paths additionally having the same sequence of extracted fluid flow rates of the respective continuous places (we assume that each of the two LFSPNs has exactly one continuous place) in the corresponding discrete markings. Besides the need to respect a fluid flow in the equivalence definition, the intuition behind such a double parameterizing by the average sojourn times and by the fluid flow rates is as follows. In each of the corresponding discrete markings of the comparable paths we shall have the same average potential fluid change volume in the corresponding continuous places, which is a product of the average sojourn time and the constant (possibly zero or negative) potential fluid flow rate.

We show that fluid trace equivalence preserves average potential fluid change volume in the respective continuous places for the transition sequences of each particular length.

Second, we propose a branching-time relation of fluid bisimulation equivalence on LFSPNs. We prove that it is strictly stronger than fluid trace equivalence, i.e. the former relation generally makes less identifications among the compared LFSPNs than the latter. We require the fluid bisimulation on the discrete markings of two LFSPNs to be a standard (strong) Markovian bisimulation. Hence, for each transition firing in an LFSPN, we require a simulation of the firing in the equivalent LFSPN, such that the action labels of the both fired transitions and their overall rates coincide. Thus, our definition of the bisimulation equivalence on the discrete markings of LFSPNs is similar to that of the performance bisimulation equivalences [27, 28] on labeled CTSPNs and labeled generalized SPNs (GSPNs) [61, 34, 62, 25, 14, 15], as well as the strong equivalence from [54] on stochastic process algebra PEPA. All these relations belong to the family of Markovian bisimulation equivalences, investigated on sequential and concurrent Markovian process calculi SMPC and CMPC in [18, 16, 17, 19], as well as on Uniform Labeled Transition Systems (ULTraS) in [20, 21].

As for the continuous markings, we should fix a bijective correspondence between the sets of continuous places of the two LFSPNs, hence, the number of their continuous places should coincide. Then each continuous place in the first LFSPN should have exactly one corresponding continuous place in the second LFSPN and vice versa. We require that, for every pair of the Markovian bisimilar discrete markings, the fluid flow rates of the continuous places in the first LFSPN should coincide with those of the corresponding continuous places in the second LFSPN. Note that in our formal definition of fluid bisimulation, we consider only LFSPNs having a single continuous place, since the definition can be easily extended to the case of several continuous places.

We prove that the resulting fluid bisimulation equivalence of LFSPNs preserves, for the equivalence classes of their discrete markings, the stationary probability distribution of the underlying continuous time Markov chain (CTMC), as well as the stationary fluid buffer empty probability, probability distribution and density for the associated stochastic fluid model (SFM). As a consequence, the equivalence guarantees identity of a number of discrete and hybrid performance measures, calculated for the stationary quantitative behaviour of the LFSPNs. The fluid bisimulation equivalence is then used to simplify the qualitative and quantitative analysis of LFSPNs, due to diminishing the number of discrete markings considered that are lumped into the equivalence classes, interpreted as the (aggregate) states of the quotient discrete reachability graph and quotient underlying CTMC. We also define the quotients of the probability functions by the equivalence, aiming at description of the quotient associated SFM. Based on the pointed equivalence, a new quotient technique enhances and optimizes the performance evaluation of fluid systems modeled by LFSPNs.

The running example presented in the paper explains systematically the most important definitions introduced. It also demonstrates in detail the functional and performance identity of the LFSPNs, related by fluid trace or fluid bisimulation equivalence. The application example consists in a case study of three LFSPNs, each of them modeling the document preparation system, and demonstrates how the LFSPNs structure and behaviour can be reduced with respect to fluid bisimulation equivalence while preserving their functional and performance properties.

1.4 Logical characterization of the fluid equivalences

A characterization of equivalences via modal logics is used to change the operational reasoning on systems behaviour by the logical one that is more appropriate for verification. Moreover, such an interpretation elucidates the nature of the equivalences, defined in an operational manner. It is generally accepted that the natural and nice modal characterization of a behavioural equivalence justifies its relevance. On the other hand, we get an operational characterization of logical equivalences. The importance of modal logical characterization for behavioural equivalences has been explained in [2], in particular, the resulting capabilities to express distinguishing formulas for automatic verification of systems [58] and characteristic formulas for the equivalence classes of processes [68, 4], to demonstrate finitariness and algebraicity of behavioural preorders [3], as well as to give a testing interpretation of bisimulation equivalence [1].

In the literature, several logical characterizations of stochastic and Markovian equivalences have been proposed. In [37, 38], the characterization of strong equivalence has been presented with the logic PMLμ, which is a stochastic extension of Probabilistic Modal Logic (PML) [60] on probabilistic transitions systems to the stochastic process algebra PEPA [54]. In [45], a branching time temporal logic has been described which is an extension of Continuous Stochastic Logic (CSL) [8] on CTMCs to a wide class of SFMs. The CSL-based logical characterizations of various stochastic bisimulation equivalences have been reported in [10, 11, 12, 67, 13, 23] on labeled CTMCs, in [40] on labeled continuous time Markov processes (CTMPs), in [41] on analytic spaces, in [9] on labeled Markov reward models (MRMs) and in [66] on labeled continuous time Markov decision processes (CTMDPs). In [18, 16], on sequential and concurrent Markovian process calculi SMPC (MPC) and CMPC, the logical characterizations of Markovian trace and bisimulation equivalences have been accomplished with the modal logics $HML_{MTr}$ and $HML_{MB}$, based on Hennessy-Milner Logic (HML) [53]. In [19], on (sequential) Markovian process calculus MPC, the logical characterizations of Markovian trace and bisimulation equivalences have been constructed with the HML-based modal logics $HML_{NPMTr}$ and $HML_{MB}$.

We provide fluid trace and bisimulation equivalences with the logical characterizations, accomplished via formulas of the specially constructed novel fluid modal logics $HML_{flt}$ and $HML_{flb}$, respectively. The new logics are based on Hennessy-Milner Logic (HML) [53]. The logical characterizations guarantee that two LFSPNs are fluid (trace or bisimulation) equivalent iff they satisfy the same formulas of the respective fluid modal logic, i.e. they are logically equivalent. Thus, instead of comparing LFSPNs operationally, one may only check the corresponding satisfaction relation. This provides one with the possibility for logical reasoning on fluid equivalences for LFSPNs. Such an approach is often more convenient for the purpose of verification. The obtained results may be also interpreted as operational characterizations of the corresponding logical equivalences.

The fluid modal logic $HML_{flt}$ is used to characterize fluid trace equivalence. Therefore, the interpretation function of the logic has an additional argument, which is the sequence of the potential fluid flow rates for the single continuous place of an LFSPN (remember that in the standard definition of fluid trace equivalence we compare only LFSPNs, each having exactly one continuous place). In $HML_{flt}$, one can express the properties like “the execution probability of a sequence of actions starting from a state, with given average sojourn times and potential fluid flow rates in the initial, intermediate and final states, is equal to a particular value”. For example, for a production line in a food processing or a chemicals plant, we can verify the probability that the first liquid substance fills (this is specified by the action $f_{1}$) the fluid reservoir with the potential flow rate $r_{1}$ during the exponentially distributed time period with the average $s_{1}$; then the second liquid substance fills (the action $f_{2}$) the reservoir with the potential flow rate $r_{2}$ during the exponentially distributed time period with the average $s_{2}$; finally, the reservoir is emptied with the potential flow rate $r_{3}$ for the exponentially distributed time period with the average $s_{3}$.

The fluid modal logic $HML_{flb}$ is intended to characterize fluid bisimulation equivalence. For this purpose, the logic has a new modality, decorated with the potential fluid flow rate value for the single continuous place of an LFSPN (again, remember that in the standard definition of fluid bisimulation equivalence consider only LFSPNs, each having a single continuous place). The resulting formula (i.e. the new modality with the flow rate value) is used to check whether the potential fluid flow rate in a discrete marking of an LFSPN coincides with a certain value, the fact that corresponds to a condition from the fluid bisimulation definition. Thus, $HML_{flb}$ is able to describe the properties such as “an action can be executed with a given minimal rate in a state with a given potential fluid flow rate”. For example, for the production line mentioned above, we can verify the validity that the first liquid substance fills (the action $f_{1}$) the fluid reservoir with the potential flow rate $r_{1}$ during the exponentially distributed time period with the rate $\lambda_{1}$ or the second liquid substance fills (the action $f_{2}$) the reservoir with the same potential flow rate $r_{1}$ during the exponentially distributed time period with the rate $\lambda_{2}$. Note that disjunction in $HML_{flb}$ can be defined standardly, i.e. using conjunction and negation.

1.5 Previous works and contributions of the paper

The first results on this subject can be found in [73], where we have proposed a class of LFSPNs and defined a novel behavioural relation of fluid bisimulation equivalence for them. We have also proven there that the equivalence preserves aggregate fluid density and distribution, as well as discrete and continuous performance measures. The present paper is an improved and extended version of that publication. The paper contains the following new results for LFSPNs: fluid trace equivalence, interrelations of the fluid equivalences, quotienting by fluid bisimulation equivalence, logical characterization of the fluid equivalences, quotients of the probability functions and an application example.

Thus, the main contributions of the paper are as follows.

• •

LFSPNs extend FSPNs with the action labeling on their transitions, which allows for the functional behavioural reasoning.

• •

Fluid trace and bisimulation equivalences permit to compare and reduce the qualitative and quantitative behaviour of LFSPNs in the the linear-time and branching-time semantics, respectively.

• •

The analysis of LFSPNs is simplified by quotienting their discrete reachability graphs and underlying CTMCs by fluid bisimulation equivalence.

• •

Fluid trace and bisimulation equivalences are logically characterized via two original fluid modal logics $HML_{flt}$ and $HML_{flb}$.

• •

The aggregate probability functions coincide as for the discrete part (labeled CTSPNs and their underlying CTMCs), as for the continuous part (SFMs) of the fluid bisimulation equivalent LFSPNs.

• •

Both the discrete and hybrid performance measures for LFSPNs are preserved by fluid bisimulation equivalence.

• •

Application example shows in detail the functional and performance identity of the fluid bisimulation equivalent LFSPNs specifying the document preparation system.

1.6 Outline of the paper

The rest of the paper is organized as follows. In Section 2, we present the definition and behaviour of LFSPNs. Section 3 explores the discrete part of LFSPNs, i.e. the derived labeled CTSPNs and their underlying CTMCs. Section 4 investigates the continuous part of LFSPNs, which is the associated SFMs. In Section 5, we construct a linear-time relation of fluid trace equivalence for LFSPNs. In Section 6, we propose a branching-time relation of fluid bisimulation equivalence for LFSPNs and compare it with the fluid trace one. In Section 7, we explain how to reduce discrete reachability graphs and underlying CTMCs of LFSPNs modulo fluid bisimulation equivalence, by applying the method of the quotienting. Section 8 is devoted to the logical characterization of fluid trace and bisimulation equivalences with the use of two novel fluid modal logics. Section 9 contains the preservation results for the quantitative behaviour of LFSPNs modulo fluid bisimulation equivalence. In Section 10, we demonstrate how fluid bisimulation equivalence preserves the functionality and performance measures of LFSPNs. Section 11 describes a case study of three LFSPNs modeling the document preparation system. Finally, Section 12 summarizes the results obtained and outlines research perspectives in this area.

To help the reader, we have presented some important abbreviations from the paper in Table 1.

2 Basic concepts of LFSPNs

Let us introduce a class of labeled fluid stochastic Petri nets (LFSPNs), whose transitions are labeled with action names, used to specify different system activities. Without labels, LFSPNs are essentially a subclass of FSPNs [55, 43, 49], so that their discrete part describes CTSPNs [63, 61, 62, 14]. This means that LFSPNs have no inhibitor arcs, priorities and immediate transitions, which are used in the standard FSPNs, which are the continuous extension of GSPNs. However, in many practical applications, the performance analysis of GSPNs is simplified by transforming them into CTSPNs or reducing their underlying semi-Markov chains into CTMCs (which are the underlying stochastic process of CTSPNs) by eliminating vanishing states [34, 62, 14, 15]. Transition labeling in LFSPNs is similar to the labeling, proposed for CTSPNs in [27]. Moreover, we suppose that the firing rates of transitions and flow rates of the continuous arcs do not depend on the continuous markings (fluid levels).

Let ${\mathbb{N}}=\{0,1,2,\ldots\}$ be the set of all natural numbers and ${\mathbb{N}}_{\geq 1}=\{1,2,\ldots\}$ be the set of all positive natural numbers. Further, let ${\mathbb{R}}=(-\infty;\infty)$ be the set of all real numbers, ${\mathbb{R}}_{\geq 0}=[0;\infty)$ be the set of all non-negative real numbers and ${\mathbb{R}}_{>0}=(0;\infty)$ be the set of all positive real numbers. The set of all row vectors of $n\in{\mathbb{N}}_{\geq 1}$ elements from a set $X$ is defined as $X^{n}=\{(x_{1},\ldots,x_{n})\mid x_{i}\in X\ (1\leq i\leq n)\}$. The set of all mappings from a set $X$ to a set $Y$ is defined as $Y^{X}=\{f\mid f:X\rightarrow Y\}$. Let $Act=\{a,b,\ldots\}$ be the set of actions.

First, we present a formal definition of LFSPNs.

Definition 2.1

*A labeled fluid stochastic Petri net (LFSPN) is a tuple

$N=(P_{N},T_{N},W_{N},C_{N},R_{N},\Omega_{N},L_{N},{\cal M}_{N})$, where*

• •

$P_{N}=Pd_{N}\uplus Pc_{N}$* is a finite set of discrete and continuous places ($\uplus$ denotes disjoint union);*

• •

$T_{N}$* is a finite set of transitions, such that $P_{N}\cup T_{N}\neq\emptyset$ and $P_{N}\cap T_{N}=\emptyset$;*

• •

$W_{N}:(Pd_{N}\times T_{N})\cup(T_{N}\times Pd_{N})\rightarrow{\mathbb{N}}$* is a function providing the weights of discrete arcs between discrete places and transitions;*

• •

$C_{N}\subseteq(Pc_{N}\times T_{N})\cup(T_{N}\times Pc_{N})$* is the set of continuous arcs between continuous places and transitions;*

• •

$R_{N}:C_{N}\times{\mathbb{N}}^{|Pd_{N}|}\rightarrow{\mathbb{R}}_{\geq 0}$* is a function providing the flow rates of continuous arcs in a given discrete marking (the markings will be defined later); *

• •

$\Omega_{N}:T_{N}\times{\mathbb{N}}^{|Pd_{N}|}\rightarrow{\mathbb{R}}_{>0}$* is the transition rate function associating transitions with rates in a given discrete marking; *

• •

$L_{N}:T_{N}\rightarrow Act$* is the transition labeling function assigning actions to transitions;*

• •

${\cal M}_{N}=(M_{N},{\bf 0})$, where $M_{N}\in{\mathbb{N}}^{|Pd_{N}|}$ and ${\bf 0}$ is a row vector of $|Pc_{N}|$ values [math], is the initial (discrete-continuous) marking.

Let us consider in more detail the tuple elements from the definition above. Let $N$ be an LFSPN.

Every discrete place $p_{i}\in Pd_{N}$ may contain discrete tokens, whose amount is represented by a natural number $M_{i}\in{\mathbb{N}}\ (1\leq i\leq|Pd_{N}|)$. Each continuous place $q_{j}\in Pc_{N}$ may contain continuous fluid, with the level represented by a non-negative real number $X_{j}\in{\mathbb{R}}_{\geq 0}\ (1\leq j\leq|Pc_{N}|)$. Then the complete hybrid (discrete-continuous) marking of $N$ is a pair $(M,X)$, where $M=(M_{1},\ldots,M_{|Pd_{N}|})$ is a discrete marking and $X=(X_{1},\ldots,X_{|Pc_{N}|})$ is a continuous marking. When needed, these vectors can also be seen as the mappings $M:Pd_{N}\rightarrow{\mathbb{N}}$ with $M(p_{i})=M_{i}\ (1\leq i\leq|Pd_{N}|)$ and $X:Pc_{N}\rightarrow{\mathbb{R}}_{\geq 0}$ with $X(q_{j})=X_{j}\ (1\leq j\leq|Pc_{N}|)$. The set of all markings (reachability set) of $N$ is denoted by $RS(N)$. Then $DRS(N)=\{M\mid(M,X)\in RS(N)\}$ is the set of all discrete markings (discrete reachability set) of $N$. $DRS(N)$ will be formally defined later. Further, $CRS(N)=\{X\mid(M,X)\in RS(N)\}\subseteq{\mathbb{R}}_{\geq 0}^{|Pc_{N}|}$ is the set of all continuous markings (continuous reachability set) of $N$. Every marking $(M,X)\in RS(N)$ evolves in time, hence, we can interpret it as a stochastic process $\{(M(\delta),X(\delta))\mid\delta\geq 0\}$. Then the initial marking of $N$ is that at the zero time moment, i.e. ${\cal M}_{N}=(M_{N},{\bf 0})=(M(0),X(0))$, where $X(0)={\bf 0}$ means that all the continuous places are initially empty.

Every transition $t\in T_{N}$ has a positive real instantaneous rate $\Omega_{N}(t,M)\in{\mathbb{R}}_{>0}$ associated, which is a parameter of the exponential distribution governing the transition delay (being a random variable), when the current discrete marking is $M$. Transitions are labeled with actions, each representing a sort of activity that they model.

Every discrete arc $da=(p,t)$ or $da=(t,p)$, where $p\in Pd_{N}$ and $t\in T_{N}$, connects discrete places and transitions. It has a non-negative integer-valued weight $W_{N}(da)\in{\mathbb{N}}$ assigned, representing its multiplicity. The zero weight indicates that the corresponding discrete arc does not exist, since its multiplicity is zero in this case. In the discrete marking $M\in DRS(N)$, every continuous arc $ca=(q,t)$ or $ca=(t,q)$, where $q\in Pc_{N}$ and $t\in T_{N}$, connects continuous places and transitions. It has a non-negative real-valued flow rate $R_{N}(ca,M)\in{\mathbb{R}}_{\geq 0}$ of fluid through $ca$, when the current discrete marking is $M$. The zero flow rate indicates that the fluid flow along the corresponding continuous arc is stopped in some discrete marking.

The graphical representation of LFSPNs resembles that for standard labeled Petri nets, but supplemented with the rates or weights, written near the corresponding transitions or arcs. Discrete places are drawn with ordinary circles while double concentric circles correspond to the continuous ones. Square boxes with the action names inside depict transitions and their labels. Discrete arcs are drawn as thin lines with arrows at the end while continuous arcs should represent pipes, so the latter are depicted by thick arrowed lines. If the rates or the weights are not given in the picture then they are assumed to be of no importance in the corresponding examples. The names of places and transitions are depicted near them when needed.

We now consider the behaviour of LFSPNs.

Let $N$ be an LFSPN and $M$ be a discrete marking of $N$. A transition $t\in T_{N}$ is enabled in $M$ if $\forall p\in Pd_{N}\ W_{N}(p,t)\leq M(p)$. Let $Ena(M)$ be the set of all transitions enabled in $M$. Firings of transitions are atomic operations, and only single transitions are fired at once. Note that the enabling condition depends only on the discrete part of $N$ and this condition is the same as for CTSPNs. Firing of a transition $t\in Ena(M)$ changes $M$ to another discrete marking $\widetilde{M}$, such as $\forall p\in Pd_{N}\ \widetilde{M}(p)=M(p)-W_{N}(p,t)+W_{N}(t,p)$, denoted by $M\stackrel{{\scriptstyle t}}{{\rightarrow}}_{\lambda}\widetilde{M}$, where $\lambda=\Omega_{N}(t,M)$. We write $M\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}$ if $\exists\lambda\ M\stackrel{{\scriptstyle t}}{{\rightarrow}}_{\lambda}\widetilde{M}$ and $M\rightarrow\widetilde{M}$ if $\exists t\ M\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}$.

Let us formally define the discrete reachability set of $N$.

Definition 2.2

Let $N$ be an LFSPN. The discrete reachability set of $N$, denoted by $DRS(N)$, is the minimal set of discrete markings such that

• •

$M_{N}\in DRS(N)$;

• •

if $M\in DRS(N)$ and $M\rightarrow\widetilde{M}$ then $\widetilde{M}\in DRS(N)$.

Let us now define the discrete reachability graph of $N$.

Definition 2.3

*Let $N$ be an LFSPN. The discrete reachability graph of $N$ is a labeled transition system

$DRG(N)=(S_{N},{\cal L}_{N},{\cal T}_{N},s_{N})$, where*

• •

the set of states is $S_{N}=DRS(N)$;

• •

the set of labels is ${\cal L}_{N}=T_{N}\times{\mathbb{R}}_{>0}$;

• •

the set of transitions is ${\cal T}_{N}=\{(M,(t,\lambda),\widetilde{M})\mid M,\widetilde{M}\in DRS(N),\ M\stackrel{{\scriptstyle t}}{{\rightarrow}}_{\lambda}\widetilde{M}\}$;

• •

the initial state is $s_{N}=M_{N}$.

3 Discrete part of LFSPNs

We have restricted the class of FSPNs underlying LFSPNs to those whose discrete part is CTSPNs, since the performance analysis of standard FSPNs with GSPNs as the discrete part is finally based on the CTMCs which are extracted from the underlying semi-Markov chains (SMCs) of the GSPNs by removing vanishing states. Let us now consider the behaviour of the discrete part of LFSPNs, which is labeled CTSPNs.

For an LFSPN $N$, a continuous random variable $\xi(M)$ is associated with every discrete marking $M\in DRS(N)$. The variable captures a residence (sojourn) time in $M$. We adopt the race semantics, in which the fastest stochastic transition (i.e. that with the minimal exponentially distributed firing delay) fires first. Hence, the probability distribution function (PDF) of the sojourn time in $M$ is that of the minimal firing delay of transitions from $Ena(M)$. Since exponential distributions are closed under minimum, the sojourn time in $M$ is (again) exponentially distributed with a parameter that is called the exit rate from the discrete marking $M$, defined as

[TABLE]

Note that we may have $RE(M)=0$, meaning that there is no exit from $M$, if it is a terminal discrete marking, i.e. there are no transitions from it to different discrete markings.

Hence, the PDF of the sojourn time in $M$ (the probability of the residence time in $M$ being less than $\delta$) is $F_{\xi(M)}(\delta)={\sf P}(\xi(M)<\delta)=1-e^{-RE(M)\delta}\ (\delta\geq 0)$. Then the probability density function of the residence time in $M$ (the limit probability of staying in $M$ at the time $\delta$) is $f_{\xi(M)}(\delta)=\lim_{\Delta\to 0}\frac{F_{\xi(M)}(\delta+\Delta)-F_{\xi(M)}(\delta)}{\Delta}=\frac{dF_{\xi(M)}(\delta)}{d\delta}=RE(M)e^{-RE(M)\delta}\ (\delta\geq 0)$. The mean value (average, expectation) formula for the exponential distribution allows us to calculate the average sojourn time in $M$ as ${\sf M}({\xi(M)})=\int_{0}^{\infty}\delta f_{\xi(M)}(\delta)d\delta=\frac{1}{RE(M)}$. The variance (dispersion) formula for the exponential distribution allows us to calculate the sojourn time variance in $M$ as ${\sf D}({\xi(M)})=\int_{0}^{\infty}(\delta-{\sf M}({\xi(M)}))^{2}f_{\xi(M)}(\delta)d\delta=\frac{1}{(RE(M))^{2}}$. We are now ready to present the following two definitions.

The average sojourn time in the discrete marking $M$ is

[TABLE]

The average sojourn time vector of $N$, denoted by $SJ$, has the elements $SJ(M),\ M\in DRS(N)$.

Note that we may have $SJ(M)=\infty$, meaning that we stay in $M$ forever, if it is a terminal discrete marking.

The sojourn time variance in the discrete marking $M$ is

[TABLE]

The sojourn time variance vector of $N$, denoted by $VAR$, has the elements $VAR(M),\ M\in DRS(N)$.

Note that we may have $VAR(M)=\infty$, meaning that the variance of the infinite sojourn time in $M$ is infinite too, if it is a terminal discrete marking.

To evaluate performance with the use of the discrete part of $N$, we should investigate the stochastic process associated with it. The process is the underlying continuous time Markov chain, denoted by $CTMC(N)$.

Let $M,\widetilde{M}\in DRS(N)$. The rate of moving from $M$ to $\widetilde{M}$ by firing any transition is

[TABLE]

Definition 3.1

Let $N$ be an LFSPN. The underlying continuous time Markov chain (CTMC) of $N$, denoted by $CTMC(N)$, has the state space $DRS(N)$, the initial state $M_{N}$ and the transitions $M\rightarrow_{\lambda}\widetilde{M}$, if $M\rightarrow\widetilde{M}$, where $\lambda=RM(M,\widetilde{M})$.

Isomorphism is a coincidence of systems up to renaming their components or states. Let $\simeq$ denote isomorphism between CTMCs that binds their initial states.

Let $N$ be an LFSPN. The elements ${\cal Q}_{ij}\ (1\leq i,j\leq n=|DRS(N)|)$ of the transition rate matrix (TRM), also called infinitesimal generator, ${\bf Q}$ for $CTMC(N)$ are defined as

[TABLE]

The transient probability mass function (PMF) $\varphi(\delta)=(\varphi_{1}(\delta),\ldots,\varphi_{n}(\delta))$ for $CTMC(N)$ is calculated via matrix exponent as

[TABLE]

where $\varphi(0)=(\varphi_{1}(0),\ldots,\varphi_{n}(0))$ is the initial PMF, defined as

[TABLE]

The steady-state PMF $\varphi=(\varphi_{1},\ldots,\varphi_{n})$ for $CTMC(N)$ is a solution of the linear equation system

[TABLE]

where ${\bf 0}$ is a row vector of $n$ values [math] and ${\bf 1}$ is that of $n$ values $1$.

Note that the vector $\varphi$ exists and is unique, if $CTMC(N)$ is ergodic. Then $CTMC(N)$ has a single steady state, and we have $\varphi=\lim_{\delta\to\infty}\varphi(\delta)$.

Let $N$ be an LFSPN. The following steady-state discrete performance indices (measures) can be calculated based on the steady-state PMF $\varphi$ for $CTMC(N)$ [63, 61, 34, 25, 62, 14, 15].

• •

The fraction (proportion) of time spent in the set of discrete markings $S\subseteq DRS(N)$ is

[TABLE]

• •

The probability that $k\geq 0$ tokens are contained in a discrete place $p\in Pd_{N}$ is

[TABLE]

Then the PMF of the number of tokens in $p$ is $Tokens(p)=(Tokens(p,0),Tokens(p,1),\ldots)$.

• •

The probability of event ${\cal A}$ defined through (a condition that holds for all discrete markings from) the set of discrete markings $DRS_{\cal A}(N)\subseteq DRS(N)$ is

[TABLE]

• •

The average number of tokens in a discrete place $p\in Pd_{N}$ is

[TABLE]

• •

The firing frequency (throughput) of a transition $t\in T_{N}$ (average number of firings per unit of time) is

[TABLE]

• •

The exit/entrance frequency of a discrete marking $M_{i}\in DRS(N)\ (1\leq i\leq n)$ (average number of exits/entrances per unit of time) is

[TABLE]

• •

The probability of the event determined by a reward function $r(M_{i})=r_{i}\ (0\leq r_{i}\leq 1,\ 1\leq i\leq n)$ of the discrete markings is

[TABLE]

• •

The traversal frequency of the move from a discrete marking $M_{i}$ to a discrete marking $M_{j}\in DRS(N)\ (1\leq i,j\leq n)$ (average number of traversals per unit of time) is

[TABLE]

• •

Let $TravTokens$ be the average number of tokens traversing a subnet of $N$ and $Rate$ be the average input (output) token rate into (out of) the subnet. The average delay of a token traversing the subnet is

[TABLE]

4 Continuous part of LFSPNs

We now consider the impact the discrete part of LFSPNs has on their continuous part, which is stochastic fluid models (SFMs). We investigate LFSPNs with a single continuous place, since the definitions and our subsequent results on the fluid bisimulation can be transferred straightforwardly to the case of several continuous places, where multidimensional SFMs have to be explored.

Let $N$ be an LFSPN such that $Pc_{N}=\{q\}$ and $M(\delta)\in DRS(N)$ be its discrete marking at the time $\delta\geq 0$. Every continuous arc $ca=(q,t)$ or $ca=(t,q)$, where $t\in T_{N}$, changes the fluid level in the continuous place $q$ at the time $\delta$ with the flow rate $R_{N}(ca,M(\delta))$. This means that in the discrete marking $M(\delta)$ fluid can leave $q$ along the continuous arc $(q,t)$ with the rate $R_{N}((q,t),M(\delta))$ and can enter $q$ along the continuous arc $(t,q)$ with the rate $R_{N}((t,q),M(\delta))$ for every transition $t\in Ena(M(\delta))$.

The potential rate of the fluid level change (fluid flow rate) for the continuous place $q$ in the discrete marking $M(\delta)$ is

[TABLE]

Let $X(\delta)$ be the fluid level in $q$ at the time $\delta$. It is clear that the fluid level in a continuous place can never be negative. Therefore, $X(\delta)$ satisfies the following ordinary differential equation describing the actual fluid flow rate for the continuous place $q$ in the marking $(M(\delta),X(\delta))$:

[TABLE]

In the first case considered in the definition above, we have $X(\delta)=0$. In this case, if $RP(M(\delta))\geq 0$ then the fluid level is growing and the derivative is equal to the potential rate. Otherwise, if $RP(M(\delta))<0$ then we should prevent the fluid level from crossing the lower boundary (zero) by stopping the fluid flow. For an explanation of the more complex second and third cases please refer to [42, 55, 43, 49]. Note that $\frac{dX(\delta)}{d\delta}$ is a piecewise constant function of $X(\delta)$; hence, for each different “constant” segment we have $\frac{dX(\delta)}{d\delta}=RP(M(\delta))$ or $\frac{dX(\delta)}{d\delta}=0$ and, therefore, we can suppose that within each such segment $RP(M(\delta))$ or [math] are the actual fluid flow rates for the continuous place $q$ in the marking $(M(\delta),X(\delta))$. While constructing differential equations that describe the behaviour of SFMs associated with LFSPNs, we are interested only in the segments where $\frac{dX(\delta)}{d\delta}=RP(M(\delta))$. The SFMs behaviour within the remaining segments, where $\frac{dX(\delta)}{d\delta}=0$, is completely comprised by the buffer empty probability function that collects the probability mass at the lower boundary.

The elements ${\cal R}_{ij}\ (1\leq i,j\leq n=|DRS(N)|)$ of the fluid rate matrix (FRM) ${\bf R}$ for the continuous place $q$ are defined as

[TABLE]

According to [43, 49], the underlying SFMs of LFSPNs are the first order, infinite buffer, homogeneous Markov fluid models. The discrete part of the SFM derived from an LFSPN $N$ is the CTMC $CTMC(N)$ with the TRM ${\bf Q}$. The evolution of the continuous part of the SFM (the fluid flow drift) is described by the FRM ${\bf R}$.

Let us consider the transient behaviour of the SFM associated with an LFSPN $N$. We introduce the following transient probability functions.

• •

$\varphi_{i}(\delta)={\sf P}(M(\delta)=M_{i})$ is the discrete marking probability;

• •

$\ell_{i}(\delta)={\sf P}(X(\delta)=0,\ M(\delta)=M_{i})$ is the buffer empty probability (probability mass at the lower boundary);

• •

$F_{i}(\delta,x)={\sf P}(X(\delta)<x,\ M(\delta)=M_{i})$ is the fluid probability distribution function;

• •

$f_{i}(\delta,x)=\frac{\partial F_{i}(\delta,x)}{\partial x}=\lim_{h\to 0}\frac{F_{i}(\delta,x+h)-F_{i}(\delta,x)}{h}=\lim_{h\to 0}\frac{{\sf P}(x<X(\delta)<x+h,\ M(\delta)=M_{i})}{h}$ is the fluid probability density function.

The initial conditions are:

[TABLE]

[TABLE]

[TABLE]

Let $\varphi(\delta),\ell(\delta),F(\delta,x),f(\delta,x)$ be the row vectors with the elements $\varphi_{i}(\delta),\ell_{i}(\delta),F_{i}(\delta,x),f_{i}(\delta,x)$, respectively $(1\leq i\leq n)$.

By the total probability law, we have

[TABLE]

The partial differential equations describing the transient behaviour are

[TABLE]

[TABLE]

Note that we have $\frac{\partial F(\delta,x)}{\partial x}=f(\delta,x),\ F(\delta,0)=\ell(\delta),\ F(\delta,\infty)=\varphi(\delta)$.

The partial differential equation for the buffer empty probabilities (lower boundary conditions) are

[TABLE]

The lower boundary constraint is: if ${\cal R}_{ii}=RP(M_{i})>0$ then $\ell_{i}(\delta)=F_{i}(\delta,0)=0\ (1\leq i\leq n)$.

The normalizing condition is

[TABLE]

where ${\bf 1}$ is a row vector of $n$ values $1$.

Let us now consider the stationary behaviour of the SFM associated with an LFSPN $N$. We do not discuss here in detail the conditions under which the steady state for the associated SFM exists and is unique, since this topic has been extensively explored in [55, 43, 49]. Particularly, according to [55, 49], the steady-state PDF exists (i.e. the transient functions approach their stationary values, as the time parameter $\delta$ tends to infinity in the transient equations), when the associated SFM is a Markov fluid model, whose fluid flow drift (described by the matrix ${\bf R}$) and transition rates (described by the matrix ${\bf Q}$) are fluid level independent, and the following stability condition holds:

[TABLE]

stating that the steady-state mean potential fluid flow rate for the continuous place $q$ is negative. Stable infinite buffer models usually converge, hence, the existing steady-state PDF is also unique in this case.

We introduce the following steady-state probability functions, obtained from the transient ones by taking the limit $\delta\to\infty$.

• •

$\varphi_{i}=\lim_{\delta\to\infty}{\sf P}(M(\delta)=M_{i})$ is the steady-state discrete marking probability;

• •

$\ell_{i}=\lim_{\delta\to\infty}{\sf P}(X(\delta)=0,\ M(\delta)=M_{i})$ is the steady-state buffer empty probability (probability mass at the lower boundary);

• •

$F_{i}(x)=\lim_{\delta\to\infty}{\sf P}(X(\delta)<x,\ M(\delta)=M_{i})$ is the steady-state fluid probability distribution function;

• •

$f_{i}(x)=\frac{dF_{i}(x)}{dx}=\lim_{h\to 0}\frac{F_{i}(x+h)-F_{i}(x)}{h}=\lim_{\delta\to\infty}\lim_{h\to 0}\frac{{\sf P}(x<X(\delta)<x+h,\ M(\delta)=M_{i})}{h}$ is the steady-state fluid probability density function.

Let $\varphi,\ell,F(x),f(x)$ be the row vectors with the elements $\varphi_{i},\ell_{i},F_{i}(x),f_{i}(x)$, respectively $(1\leq i\leq n)$.

By the total probability law for the stationary behaviour, we have

[TABLE]

The ordinary differential equations describing the stationary behaviour are

[TABLE]

[TABLE]

Note that we have $\frac{dF(x)}{dx}=f(x),\ F(0)=\ell,\ F(\infty)=\varphi$.

The ordinary differential equation for the steady-state buffer empty probabilities (stationary lower boundary conditions) are

[TABLE]

The stationary lower boundary constraint is: if ${\cal R}_{ii}=RP(M_{i})>0$ then $F_{i}(0)=\ell_{i}=0\ (1\leq i\leq n)$.

The stationary normalizing condition is

[TABLE]

where ${\bf 1}$ is a row vector of $n$ values $1$.

The solutions of the equations for $F(x)$ and $f(x)$ in the form of matrix exponent are $F(x)=\ell e^{x{\bf Q}{\bf R}^{-1}}$ and $f(x)=\ell{\bf Q}{\bf R}^{-1}e^{x{\bf Q}{\bf R}^{-1}}$, respectively. Since the steady-state existence implies boundedness of the SFM associated with an LFSPN and we do not have a finite upper fluid level bound, the positive eigenvalues of ${\bf Q}{\bf R}^{-1}$ must be excluded. Moreover, ${\bf R}^{-1}$ does not exist if for some $i\ (1\leq i\leq n)$ we have ${\cal R}_{ii}=0$. These difficulties are avoided in the alternative solution method for $F(x)$, called spectral decomposition [76, 55, 43, 49, 46], which we outline below.

Let us define the sets of negative discrete markings of $N$ as $DRS^{-}(N)=\{M\in DRS(N)\mid RP(M)<0\}$, zero discrete markings of $N$ as $DRS^{0}(N)=\{M\in DRS(N)\mid RP(M)=0\}$ and positive discrete markings of $N$ as $DRS^{+}(N)=\{M\in DRS(N)\mid RP(M)>0\}$. The spectral decomposition is $F(x)=\sum_{j=1}^{m}a_{j}e^{\gamma_{j}x}v_{j}$, where $a_{j}$ are some scalar coefficients, $\gamma_{j}$ are the eigenvalues and $v_{j}=(v_{j1},\ldots,v_{jn})$ are the eigenvectors of ${\bf Q}{\bf R}^{-1}$. Thus, each $v_{j}$ is the solution of the equation $v_{j}({\bf Q}{\bf R}^{-1}-\gamma_{j}{\bf I})=0$, where ${\bf I}$ is the identity matrix of the order $n$, hence, it holds $v_{j}({\bf Q}-\gamma_{j}{\bf R})=0$.

Since for each non-zero $v_{j}$ we must have $|{\bf Q}-\gamma_{j}{\bf R}|=0$, the number of solutions $\gamma_{1},\ldots,\gamma_{m}$ is the number of non-zero elements among ${\cal R}_{ii}=RP(M_{i})\ (1\leq i\leq n)$, i.e. $m=|DRS^{-}(N)|+|DRS^{+}(N)|$. We have $1$ zero eigenvalue, $|DRS^{+}(N)|$ eigenvalues with a negative real part and $|DRS^{-}(N)|-1$ eigenvalues with a positive real part. Let us reorder all the eigenvalues according to the sign of their real part (first, with a zero real part; then with a negative one; at last, with a positive one). The boundedness of $F(x)$ requires $a_{j}=0$ if $Re({\gamma_{j}})>0\ (1\leq j\leq m)$. Further, for the zero eigenvalue $\gamma_{1}=0$ we have $a_{1}e^{\gamma_{1}x}v_{1}=a_{1}v_{1}$, and for the corresponding eigenvector it holds $v_{1}{\bf Q}=0$. Then $F(x)=a_{1}v_{1}+\sum_{k=2}^{|DRS^{+}(N)|+1}a_{k}e^{\gamma_{k}x}v_{k}$, where $Re({\gamma_{k}})<0\ (2\leq k\leq|DRS^{+}(N)|+1)$. Remember that $\varphi=F(\infty)=a_{1}v_{1}$, hence, $F(x)=\varphi+\sum_{k=2}^{|DRS^{+}(N)|+1}a_{k}e^{\gamma_{k}x}v_{k}$.

It remains to find $|DRS^{+}(N)|$ coefficients $a_{k}$ corresponding to the eigenvalues $\gamma_{k}\ (2\leq k\leq|DRS^{+}(N)|+1)$. Remember the stationary lower boundary constraint: if ${\cal R}_{ll}=RP(M_{l})>0$ then $F_{l}(0)=\ell_{l}=0$. Then for each positive discrete marking $M_{l}\in DRS^{+}(N)$ we have $F_{l}(0)=\varphi_{l}+\sum_{k=2}^{|DRS^{+}(N)|+1}a_{k}v_{kl}=0$. We obtain a system of $|DRS^{+}(N)|$ independent linear equations with $|DRS^{+}(N)|$ unknowns, for which a unique solution exists.

Then, using $F(x)$, we can find $f(x)=\frac{dF(x)}{dx}$ and $\ell=F(0)$.

Let $N$ be an LFSPN. The following steady-state hybrid (discrete-continuous) performance indices (measures) can be calculated based on the steady-state fluid probability density function $f(x)$ for the SFM of $N$ [24, 47, 48, 44, 43, 56]. Note that the hybrid performance indices that do not depend on the fluid level coincide with the corresponding discrete performance measures.

• •

The fraction (proportion) of time spent in the set of discrete markings $S\subseteq DRS(N)$ is

[TABLE]

• •

The probability that $k\geq 0$ tokens are contained in a discrete place $p\in Pd_{N}$ is

[TABLE]

Then the PMF of the number of tokens in $p$ is $Tokens(p)=(Tokens(p,0),Tokens(p,1),\ldots)$.

• •

The probability of the event ${\cal A}$ defined through (a condition that holds for all discrete markings from) the set of discrete markings $DRS_{\cal A}(N)\subseteq DRS(N)$ is

[TABLE]

• •

The average number of tokens in a discrete place $p\in Pd_{N}$ is

[TABLE]

• •

The firing frequency (throughput) of a transition $t\in T_{N}$ (average number of firings per unit of time) is

[TABLE]

• •

The exit/entrance frequency of a discrete marking $M_{i}\in DRS(N)\ (1\leq i\leq n)$ (average number of exits/entrances per unit of time) is

[TABLE]

• •

The mean potential fluid flow rate for the continuous place $q\in Pc_{N}$ is

[TABLE]

• •

The probability of the event determined by a reward function $r(M_{i})=r_{i}\ (0\leq r_{i}\leq 1,\\ 1\leq i\leq n)$ of the discrete markings is

[TABLE]

• •

The traversal frequency of the move from a discrete marking $M_{i}$ to a discrete marking $M_{j}\in DRS(N)\ (1\leq i,j\leq n)$ (average number of traversals per unit of time) is

[TABLE]

• •

The probability of a positive fluid level in a continuous place $q\in Pc_{N}$ is

[TABLE]

• •

The probability that the fluid level in a continuous place $q\in Pc_{N}$ does not lie below the value $v\in{\mathbb{R}}_{>0}$ is

[TABLE]

• •

The mean proportional flow rate across a continuous arc $(q,t),\ q\in Pc_{N},t\in T_{N}$, is

[TABLE]

where $R_{N}^{*}((q,t),(M,x))$ is the fluid level dependent proportional flow rate function in the marking $(M,x)\in RS(N)$, defined as

[TABLE]

Thus,

[TABLE]

• •

The mean proportional flow rate across a continuous arc $(t,q),\ t\in T_{N},\ q\in Pc_{N}$, is

[TABLE]

where $R_{N}^{*}((t,q),(M,x))$ is the fluid level dependent proportional flow rate function in the marking $(M,x)\in RS(N)$, defined as

[TABLE]

Thus,

[TABLE]

• •

The probability of the event determined by a hybrid reward function $r(M_{i},x)=r_{i}(x)\ (0\leq r_{i}(x)\leq 1,\ 1\leq i\leq n)$ of the markings is

[TABLE]

5 Fluid trace equivalence

Trace equivalences are the least discriminating ones. In the trace semantics, the behavior of a system is associated with the set of all possible sequences of actions, i.e. the protocols of work or computations. Thus, the points of choice of an external observer between several extensions of a particular computation are not taken into account.

The formal definition of fluid trace equivalence resembles that of ordinary Markovian trace equivalence, proposed on transition-labeled CTMCs in [83], on sequential and concurrent Markovian process calculi SMPC and CMPC in [18, 16, 17, 19] and on Uniform Labeled Transition Systems (ULTraS) in [20, 21]. While defining fluid trace equivalence, we additionally have to take into account the fluid flow rates in the corresponding discrete markings of two compared LFSPNs. Hence, in order to construct fluid trace equivalence, we should determine how to calculate the cumulative execution probabilities of all the specific (selected) paths. A path in the discrete reachability graph of an LFSPN is a sequence of its discrete markings and transitions that is generated by some firing sequence in the LFSPN.

First, we should multiply the transition firing probabilities for all the transitions along the paths starting in the initial discrete marking of the LFSPN. The resulting product will be the execution probability of the path. Second, we should sum the path execution probabilities for all the selected paths corresponding to the same sequence of actions, moreover, to the same sequence of the average sojourn times and the same sequence of the fluid flow rates in all the discrete markings participating the paths. We suppose that each LFSPN has exactly one continuous place. The resulting sum will be the cumulative execution probability of the selected paths corresponding to some fluid stochastic trace. A fluid stochastic trace is a pair with the first element being the triple of the correlated sequences of actions, average sojourn times and fluid flow rates, and the second element being the execution probability of the triple. Each element of the triple guarantees that fluid trace equivalence respects the following important aspects of the LFSPNs behaviour: functional activity, stochastic timing and fluid flow.

It is also possible to define fluid trace equivalence between LFSPNs with more than one continuous place, if they have the same number of the corresponding continuous places. Then one should consider the sequences of the vectors of the average sojourn times and vectors of the fluid flow rates. The elements of each such a vector will be the average sojourn times or fluid flow rates, respectively, for all continuous places in a particular discrete marking.

Note that $CTMC(N)$ can be interpreted as a semi-Markov chain (SMC) [59], denoted by $SMC(N)$, which is analyzed by extracting from it the embedded (absorbing) discrete time Markov chain (EDTMC) corresponding to $N$, denoted by $EDTMC(N)$. The construction of the latter is analogous to that applied in the context of GSPNs in [61, 62, 14, 15]. $EDTMC(N)$ only describes the state changes of $SMC(N)$ while ignoring its time characteristics. Thus, to construct the EDTMC, we should abstract from all time aspects of behaviour of the SMC, i.e. from the sojourn time in its states. It is well-known that every SMC is fully described by the EDTMC and the state sojourn time distributions (the latter can be specified by the vector of PDFs of residence time in the states) [51].

We first propose some helpful definitions of the probability functions for the transition firings and discrete marking changes. Let $N$ be an LFSPN, $M,\widetilde{M}\in DRS(N)$ be its discrete markings and $t\in Ena(M)$.

The (time-abstract) probability that the transition $t$ fires in $M$ is

[TABLE]

We have $\forall M\in{\mathbb{N}}^{|Pd_{N}|}\ \sum_{t\in Ena(M)}PT(t,M)=\sum_{t\in Ena(M)}\frac{\Omega_{N}(t,M)}{\sum_{u\in Ena(M)}\Omega_{N}(u,M)}=\frac{\sum_{t\in Ena(M)}\Omega_{N}(t,M)}{\sum_{u\in Ena(M)}\Omega_{N}(u,M)}=1$, i.e. $PT(t,M)$ defines a probability distribution.

The probability to move from $M$ to $\widetilde{M}$ by firing any transition is

[TABLE]

We write $M\rightarrow_{\cal P}\widetilde{M}$, if $M\rightarrow\widetilde{M}$, where ${\cal P}=PM(M,\widetilde{M})$. We have $\forall M\in{\mathbb{N}}^{|Pd_{N}|}\ \sum_{\{\widetilde{M}\mid M\rightarrow\widetilde{M}\}}PM(M,\widetilde{M})=\sum_{\{\widetilde{M}\mid M\rightarrow\widetilde{M}\}}\sum_{\{t\mid M\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}\}}PT(t,M)=\sum_{t\in Ena(M)}PT(t,M)=1$, i.e. $PM(M,\widetilde{M})$ defines a probability distribution.

Definition 5.1

Let $N$ be an LFSPN. The embedded (absorbing) discrete time Markov chain (EDTMC) of $N$, denoted by $EDTMC(N)$, has the state space $DRS(N)$, the initial state $M_{N}$ and the transitions $M\rightarrow_{\cal P}\widetilde{M}$, if $M\rightarrow\widetilde{M}$, where ${\cal P}=PM(M,\widetilde{M})$.

The underlying SMC of $N$, denoted by $SMC(N)$, has the EDTMC $EDTMC(N)$ and the sojourn time in every $M\in DRS(N)$ is exponentially distributed with the parameter $RE(M)$.

Since the sojourn time in every $M\in DRS(N)$ is exponentially distributed, we have $SMC(N)=CTMC(N)$.

Let $N$ be an LFSPN. The elements ${\cal P}_{ij}\ (1\leq i,j\leq n=|DRS(N)|)$ of the (one-step) transition probability matrix (TPM) ${\bf P}$ for $EDTMC(N)$ are defined as

[TABLE]

Let $X$ be a set, $n\in{\mathbb{N}}_{\geq 1}$ and $x_{i}\in X\ (1\leq i\leq n)$. Then $\chi=x_{1}\cdots x_{n}$ is a finite sequence over $X$ of length $|\chi|=n$. When $X$ is a set on numbers, we usually write $\chi=x_{1}\circ\cdots\circ x_{n}$, to avoid confusion because of mixing up the operations of concatenation of sequences ($\circ$) and multiplication of numbers ($\cdot$). The empty sequence $\varepsilon$ of length $|\varepsilon|=0$ is an extra case. Let $X^{*}$ denote the set of all finite sequences (including the empty one) over $X$.

Let $M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}\ (n\in{\mathbb{N}})$ be a finite sequence of transition firings starting in the initial discrete marking $M_{N}$ and called firing sequence in $N$. The firing sequence generates the path $M_{0}t_{1}M_{1}t_{2}\cdots t_{n}M_{n}$ in the discrete reachability graph $DRG(N)$. Since the first discrete marking $M_{N}=M_{0}$ of the path is fixed, one can see that the (finite) transition sequence $\vartheta=t_{1}\cdots t_{n}$ in $N$ uniquely determines the discrete marking sequence $M_{0}\cdots M_{n}$, ending with the last discrete marking $M_{n}$ of the mentioned path in $DRG(N)$. Hence, to refer the paths, one can simply use the transition sequences extracted from them as shown above. The empty transition sequence $\varepsilon$ refers to the path $M_{0}$, consisting just of one discrete marking (which is the first and last one of the path in such a case).

Let $N$ be an LFSPN. The set of all (finite) transition sequences in $N$ is defined as

[TABLE]

Let $\vartheta=t_{1}\cdots t_{n}\in TranSeq(N)$ and $M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}$. The probability to execute the transition sequence $\vartheta$ is

[TABLE]

For $\vartheta=\varepsilon$ we define $PT(\varepsilon)=1$. Let us prove that $\forall n\in{\mathbb{N}}\ \sum_{\{\vartheta\in TranSeq(N)\mid|\vartheta|=n\}}PT(\vartheta)=1$, i.e. $PT(\vartheta)$ defines a probability distribution.

Lemma 5.1

Let $N$ be an LFSPN. Then $\forall n\in{\mathbb{N}}$

[TABLE]

Proof. We prove by induction on the transition sequences length $n$.

• •

$n=0$

By definition, $\sum_{\{\vartheta\in TranSeq(N)\mid|\vartheta|=0\}}PT(\vartheta)=PT(\varepsilon)=1$.

• •

$n\rightarrow n+1$

By distributivity law for multiplication and addition, and since $\forall M\in{\mathbb{N}}^{|Pd_{N}|}\ \sum_{t\in Ena(M)}PT(t,M)=1$,

$\sum_{\{\vartheta\in TranSeq(N)\mid|\vartheta|=n+1\}}PT(\vartheta)=\sum_{\{t_{1},\ldots,t_{n},t_{n+1}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}\stackrel{{\scriptstyle t_{n+1}}}{{\rightarrow}}M_{n+1}\}}\prod_{i=1}^{n+1}PT(t_{i},M_{i-1})=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}\}}\sum_{\{t_{n+1}\mid M_{n}\stackrel{{\scriptstyle t_{n+1}}}{{\rightarrow}}M_{n+1}\}}\prod_{i=1}^{n}PT(t_{i},M_{i-1})PT(t_{n+1},M_{n})=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}\}}\left(\prod_{i=1}^{n}PT(t_{i},M_{i-1})\sum_{\{t_{n+1}\mid M_{n}\stackrel{{\scriptstyle t_{n+1}}}{{\rightarrow}}M_{n+1}\}}PT(t_{n+1},M_{n})\right)=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}\}}\prod_{i=1}^{n}PT(t_{i},M_{i-1})\cdot 1=1$. $\sqcap\!\!\!\!\sqcup$

Let $\vartheta=t_{1}\cdots t_{n}\in TranSeq(N)$ be a transition sequence in $N$. The action sequence of $\vartheta$ is $L_{N}(\vartheta)=a_{1}\cdots a_{n}\in Act^{*}$, where $L_{N}(t_{i})=a_{i}\ (1\leq i\leq n)$, i.e. it is the sequence of actions which label the transitions of that transition sequence. For $\vartheta=\varepsilon$ we define $L_{N}(\varepsilon)=\varepsilon$. Further, the average sojourn time sequence of $\vartheta$ is $SJ(\vartheta)=SJ(M_{0})\circ\cdots\circ SJ(M_{n})\in{\mathbb{R}}_{>0}^{*}$, i.e. it is the sequence of average sojourn times in the discrete markings of the path to which $\vartheta$ refers. For $\vartheta=\varepsilon$ we define $SJ(\varepsilon)=SJ(M_{0})$. Similarly, the (potential) fluid flow rate sequence of $\vartheta$ is $RP(\vartheta)=RP(M_{0})\circ\cdots\circ RP(M_{n})\in{\mathbb{R}}^{*}$, i.e. it is the sequence of (potential) fluid flow rates in the discrete markings of the path to which $\vartheta$ refers. For $\vartheta=\varepsilon$ we define $RP(\varepsilon)=RP(M_{0})$.

Let $N$ be an LFSPN and $(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$. The set of $(\sigma,\varsigma,\varrho)$-selected (finite) transition sequences in $N$ is defined as

[TABLE]

Let $TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset$. Then the triple $(\sigma,\varsigma,\varrho)$, together with its execution probability, which is the cumulative execution probability of all the paths from which the triple is extracted (as described above), constitute a fluid stochastic trace of the LFSPN $N$. Fluid stochastic traces are formally introduced below, followed by the (first) definition of fluid stochastic trace equivalence.

Definition 5.2

*A (finite) fluid stochastic trace of an LFSPN $N$ is a pair $((\sigma,\varsigma,\varrho),PT(\sigma,\varsigma,\varrho))$, where

$TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset$ and the (cumulative) probability to execute $(\sigma,\varsigma,\varrho)$-selected transition sequences is*

[TABLE]

We denote the set of all fluid stochastic traces of an LFSPN $N$ by $FluStochTraces(N)$. Two LFSPNs $N$ and $N^{\prime}$ are fluid trace equivalent, denoted by $N\equiv_{fl}N^{\prime}$, if

[TABLE]

By Lemma 5.1, we have $\forall n\in{\mathbb{N}}\ \sum_{\{(\sigma,\varsigma,\varrho)\mid|\sigma|=n\}}PT(\sigma,\varsigma,\varrho)=\sum_{\{(\sigma,\varsigma,\varrho)\mid|\sigma|=n\}}\sum_{\vartheta\in TranSeq(N,\sigma,\varsigma,\varrho)}PT(\vartheta)=\\ \sum_{(\sigma,\varsigma,\varrho)}\sum_{\{\vartheta\in TranSeq(N,\sigma,\varsigma,\varrho)\mid|\vartheta|=n\}}PT(\vartheta)=\sum_{\{\vartheta\in TranSeq(N)\mid|\vartheta|=n\}}PT(\vartheta)=1$, i.e. $PT(\sigma,\varsigma,\varrho)$ defines a probability distribution.

The following (second) definition of fluid stochastic trace equivalence does not use fluid stochastic traces.

Definition 5.3

Two LFSPNs $N$ and $N^{\prime}$ are fluid trace equivalent, denoted by $N\equiv_{fl}N^{\prime}$, if $\forall(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$ we have

[TABLE]

Note that in Definition 5.3, for $\vartheta=t_{1}\cdots t_{n}\in TranSeq(N,\sigma,\varsigma,\varrho)$ with $M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}$ and $\vartheta^{\prime}=t_{1}^{\prime}\cdots t_{n}^{\prime}\in TranSeq(N^{\prime},\sigma,\varsigma,\varrho)$ with $M_{N^{\prime}}=M_{0}^{\prime}\stackrel{{\scriptstyle t_{1}^{\prime}}}{{\rightarrow}}M_{1}^{\prime}\stackrel{{\scriptstyle t_{2}^{\prime}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}^{\prime}}}{{\rightarrow}}M_{n}^{\prime}$, we have $PT(\vartheta)=\prod_{i=1}^{n}PT(t_{i},M_{i-1})=\prod_{i=1}^{n}SJ(M_{i-1})\Omega_{N}(t_{i},M_{i-1})$ and $PT(\vartheta^{\prime})=\prod_{i=1}^{n}PT(t_{i}^{\prime},M_{i-1}^{\prime})=\\ \prod_{i=1}^{n}SJ(M_{i-1}^{\prime})\Omega_{N}(t_{i}^{\prime},M_{i-1}^{\prime})$. Then the equality $SJ(M_{0})\circ\cdots\circ SJ(M_{n})=SJ(\vartheta)=\varsigma=SJ(\vartheta^{\prime})=SJ(M_{0}^{\prime})\circ\cdots\circ SJ(M_{n}^{\prime})$ implies that $\prod_{i=1}^{n}SJ(M_{i-1})=\prod_{i=1}^{n}SJ(M_{i-1}^{\prime})$. Hence, $PT(\vartheta)=PT(\vartheta^{\prime})$ iff $\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})=\prod_{i=1}^{n}\Omega_{N}(t_{i}^{\prime},M_{i-1}^{\prime})$. This alternative equality results in the following (third) definition of fluid trace equivalence.

Definition 5.4

Two LFSPNs $N$ and $N^{\prime}$ are fluid trace equivalent, denoted by $N\equiv_{fl}N^{\prime}$, if $\forall(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$ we have

[TABLE]

Note that in the definition of $TranSeq(N,\sigma,\varsigma,\varrho)$, as well as in Definitions 5.2, 5.3 and 5.4, for $\vartheta\in T_{N}^{*}$, we may use the exit rate sequences $RE(\vartheta)=RE(M_{0})\circ\cdots\circ RE(M_{n})\in{\mathbb{R}}_{\geq 0}^{*}$ instead of average sojourn time sequences $\varsigma=SJ(\vartheta)=SJ(M_{0})\circ\cdots\circ SJ(M_{n})\in{\mathbb{R}}_{>0}^{*}$, since we have $\forall M\in DRS(N)\ SJ(M)=\frac{1}{RE(M)}$ and $\forall M\in DRS(N)\ \forall M^{\prime}\in DRS(N^{\prime})\ SJ(M)=SJ(M^{\prime})\ \Leftrightarrow\ RE(M)=RE(M^{\prime})$.

Let $N$ and $N^{\prime}$ be LFSPNs such that $Pc_{N}=\{q\}$ and $Pc_{N^{\prime}}=\{q^{\prime}\}$. In this case the continuous place $q^{\prime}$ of $N$ corresponds to $q$ of $N$, in other words, $q$ and $q^{\prime}$ are the respective continuous places. Then for $M\in DRS(N)$ (or for $M^{\prime}\in DRS(N^{\prime})$) we denote by $RP(M)$ (or by $RP(M^{\prime})$) the fluid level change rate for the continuous place $q$ (or for the corresponding one $q^{\prime}$), i.e. the argument discrete marking determines for which of the two continuous places, $q$ or $q^{\prime}$, the flow rate function $RP$ is taken.

Let $N$ be an LFSPN. The average potential fluid change volume in a continuous place $q\in Pc_{N}$ in the discrete marking $M\in DRS(N)$ is

[TABLE]

In order to define the probability function $PT(\sigma,\varsigma,\varrho)$, the transition sequences corresponding to a particular action sequence are also selected according to the specific average sojourn times and fluid flow rates in the discrete markings of the paths to which those transition sequences refer. One of several intuitions behind such an additional selection is as follows. The average potential fluid change volume in a continuous place $q$ in the discrete marking $M$ is a product of the average sojourn time and the constant (possibly zero or negative) potential fluid flow rate in $M$. In each of the corresponding discrete markings $M$ and $M^{\prime}$ of the paths to which the corresponding transition sequences $\vartheta\in TranSeq(N,\sigma,\varsigma,\varrho)$ and $\vartheta^{\prime}\in TranSeq(N^{\prime},\sigma,\varsigma,\varrho)$ refer, we shall have the same average potential fluid change volume in the respective continuous places $q$ and $q^{\prime}$, i.e. $FluidChange(q,M)=SJ(M)RP(M)=SJ(M^{\prime})RP(M^{\prime})=FluidChange(q^{\prime},M^{\prime})$. Note that the average actual and potential fluid change volumes coincide unless the lower boundary of fluid in some continuous place is reached, setting hereupon the actual fluid flow rate in it equal to zero till the end of the sojourn time in the current discrete marking.

Note that our notion of fluid trace equivalence is based rather on that of Markovian trace equivalence from [83], since there the average sojourn times in the states “surrounding” the actions of the corresponding traces of the equivalent processes should coincide while in the definition of the mentioned equivalence from [18, 16, 17, 19], the shorter average sojourn time may simulate the longer one. If we would adopt such a simulation then the smaller average potential fluid change volume would model the bigger one, since the potential fluid flow rate remains constant while residing in a discrete marking. Since we observe no intuition behind that modeling, we do not use it.

Let $\vartheta=t_{1}\cdots t_{n}\in TranSeq(N)$ and $M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}$. The average potential fluid change volume for the transition sequence $\vartheta$ in a continuous place $q\in Pc_{N}$ is

[TABLE]

In [20, 21], the following two types of Markovian trace equivalence have been proposed. The state-to-state Markovian trace equivalence requires coincidence of average sojourn times in all corresponding discrete markings of the paths. The end-to-end Markovian trace equivalence demands that only the sums of average sojourn times for all corresponding discrete markings of the paths should be equal. As a basis for constructing fluid trace equivalence, we have taken the state-to-state relation, since the constant potential fluid flow rate in the discrete markings may differ with their change (moreover, the actual fluid flow rate function may become discontinuous when the lower fluid boundary for a continuous place is reached in some discrete marking). Therefore, while summing the potential fluid flow rates for all discrete markings of a path, an important information is lost. The information is needed to calculate the average potential fluid change volume for a transition sequence that refers to the path. The mentioned value is a sum of the average potential fluid change volumes for all corresponding discrete markings of the path. It coincides for the corresponding transition sequences $\vartheta\in TranSeq(N,\sigma,\varsigma,\varrho)$ and $\vartheta^{\prime}\in TranSeq(N^{\prime},\sigma,\varsigma,\varrho)$, i.e. $FluidChange(q,\vartheta)=FluidChange(q^{\prime},\vartheta^{\prime})$ for the respective continuous places $q$ and $q^{\prime}$. Again, note that the average actual and potential fluid change volumes for a transition sequence may differ, due to discontinuity of the actual fluid flow rate functions for some discrete markings of the path to which the transition sequence refers.

Let $TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset$. The average potential fluid change volume for the $(\sigma,\varsigma,\varrho)$-selected (finite) transition sequences in a continuous place $q\in Pc_{N}$ is

[TABLE]

Then, as mentioned above, for the respective continuous places $q$ and $q^{\prime}$ of the LFSPNs $N$ and $N^{\prime}$, such that $TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset\neq TranSeq(N,\sigma,\varsigma,\varrho)$, we have $FluidChange(q,(\sigma,\varsigma,\varrho))=FluidChange(q^{\prime},(\sigma,\varsigma,\varrho))$.

Let $n\in{\mathbb{N}}$. The average potential fluid change volume for the transition sequences of length $n$ in a continuous place $q\in Pc_{N}$ is

[TABLE]

Note that we have $FluidChange(q,n)=\sum_{\{\vartheta\in TranSeq(N)\mid|\vartheta|=n\}}FluidChange(q,\vartheta)PT(\vartheta)=\\ \sum_{\{(\sigma,\varsigma,\varrho)\mid TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset\wedge|\sigma|=n\}}FluidChange(q,(\sigma,\varsigma,\varrho))PT(\sigma,\varsigma,\varrho)$. For the respective continuous places $q$ and $q^{\prime}$ of the LFSPNs $N$ and $N^{\prime}$ with $N\equiv_{fl}N^{\prime}$, we have $\forall n\in{\mathbb{N}}\ FluidChange(q,n)=FluidChange(q^{\prime},n)$. Thus, fluid trace equivalence preserves average potential fluid change volume for the transition sequences of every certain length in the respective continuous places.

Example 5.1

In Figure 1, the LFSPNs $N$ and $N^{\prime}$ are presented, such that $N\equiv_{fl}N^{\prime}$. We have $DRS(N)=\{M_{1},M_{2}\}$, where $M_{1}=(1,0),\ M_{2}=(0,1)$, and $DRS(N^{\prime})=\{M_{1}^{\prime},M_{2}^{\prime},M_{3}^{\prime}\}$, where $M_{1}^{\prime}=(1,0,0),\ M_{2}^{\prime}=(0,1,0),\ M_{3}^{\prime}=(0,0,1)$.

In Figure 2, the discrete reachability graphs $DRG(N)$ and $DRG(N^{\prime})$ are depicted. In Figure 3, the underlying CTMCs $CTMC(N)$ and $CTMC(N^{\prime})$ are drawn. In Figure 4, the EDTMCs $EDTMC(N)$ and $EDTMC(N^{\prime})$ are presented.

The sojourn time average and variance vectors of $N$ are

[TABLE]

The TRM ${\bf Q}$ for $CTMC(N)$, TPM ${\bf P}$ for $EDTMC(N)$ and FRM ${\bf R}$ for the SFM of $N$ are

[TABLE]

The sojourn time average and variance vectors of $N^{\prime}$ are

[TABLE]

The TRM ${\bf Q}^{\prime}$ for $CTMC(N^{\prime})$, TPM ${\bf P}^{\prime}$ for $EDTMC(N^{\prime})$ and FRM ${\bf R}^{\prime}$ for the SFM of $N^{\prime}$ are

[TABLE]

We have $t_{1}t_{2}\in TranSeq\left(N,ab,\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1\right)$ and $t_{1}t_{3}\in TranSeq\left(N,ac,\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1\right)$, hence, $FluidChange(q,t_{1}t_{2})=FluidChange(q,t_{1}t_{3})=\frac{1}{2}\cdot 1+\frac{1}{2}\cdot(-2)+\frac{1}{2}\cdot 1=0$.

We have $t_{1}^{\prime}t_{3}^{\prime}\in TranSeq\left(N^{\prime},ab,\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1\right)$ and $t_{2}^{\prime}t_{4}^{\prime}\in TranSeq\left(N^{\prime},ac,\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1\right)$, hence, $FluidChange(q^{\prime},t_{1}^{\prime}t_{3}^{\prime})=FluidChange(q^{\prime},t_{2}^{\prime}t_{4}^{\prime})=\frac{1}{2}\cdot 1+\frac{1}{2}\cdot(-2)+\frac{1}{2}\cdot 1=0$.

It holds $PT(t_{1}t_{2})=PT(t_{1}t_{3})=1\cdot\frac{1}{2}=\frac{1}{2}$ and $PT(t_{1}^{\prime}t_{3}^{\prime})=PT(t_{2}^{\prime}t_{4}^{\prime})=\frac{1}{2}\cdot 1=\frac{1}{2}$.

We get $FluStochTraces(N)=\{\left(\left(\varepsilon,\frac{1}{2},1\right),1\right),\left(\left(a,\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\right),1\right),\left(\left(ab,\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1\right),\frac{1}{2}\right),\\ \left(\left(ac,\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1\right),\frac{1}{2}\right),\ldots\}=FluStochTraces(N^{\prime})$.

It holds $FluidChange\left(q,\left(a,\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\right)\right)=FluidChange\left(q^{\prime},\left(a,\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\right)\right)=\frac{1}{2}\cdot 1+\frac{1}{2}\cdot(-2)=-\frac{1}{2}$.

We then get $FluidChange(q,1)=FluidChange(q,t_{1})PT(t_{1})=(-\frac{1}{2})\cdot 1=-\frac{1}{2}=(-\frac{1}{2})\cdot\frac{1}{2}+(-\frac{1}{2})\cdot\frac{1}{2}=FluidChange(q^{\prime},t_{1}^{\prime})PT(t_{1}^{\prime})+FluidChange(q^{\prime},t_{2}^{\prime})PT(t_{2}^{\prime})=FluidChange(q^{\prime},1)$.

In Figure 5, the ideal (since we have a stochastic process here, the actual and average sojourn times may differ) evolution of the actual fluid level for the continuous place $q$ of the LFSPN $N$ is depicted. One can see that $X(0.75)=0$, i.e. at the time moment $\delta=0.75$, the fluid level $X(\delta)$ reaches the zero low boundary while $N$ resides in the discrete marking $M(\delta)=M_{2}$ for all $\delta\in[0.5;1)$. Then the actual fluid flow rate function $RA(M(\delta),X(\delta))$ has a discontinuity at that point, where the function value is changed instantly from $-2$ to [math]. If it would exist no lower boundary, the average potential and actual fluid change volumes for the transition sequences of length $1$ in the continuous place $q$ would coincide and be equal to $FluidChange(q,1)=-0.5=0.5-1=X(1)$.

In Figure 6, possible evolution of the actual fluid level for the continuous place $q$ of the LFSPN $N$ is presented, where the actual and average sojourn times in the discrete markings demonstrate substantial differences.

6 Fluid bisimulation equivalence

Bisimulation equivalences respect particular points of choice in the behavior of a system. To define fluid bisimulation equivalence, we have to consider a bisimulation being an equivalence relation that partitions the states of the union of the discrete reachability graphs $DRG(N)$ and $DRG(N^{\prime})$ of the LFSPNs $N$ and $N^{\prime}$. For $N$ and $N^{\prime}$ to be bisimulation equivalent the initial states $M_{N}$ and $M_{N^{\prime}}$ of their discrete reachability graphs should be related by a bisimulation having the following transfer property: if two states are related then in each of them the same action can occur, leading with the identical overall rate from each of the two states to the same equivalence class for every such action.

The definition of fluid bisimulation should be given at the level of LFSPNs, but it must use the transition rates of the extracted CTMC. These rates cannot be easily (i.e. with a simple expression) defined at the level of more general LFSPNs, whose discrete part is labeled GSPNs. In addition, the action labels of immediate transitions are lost and their individual probabilities are redistributed while GSPNs are transformed into CTSPNs. The individual probabilities of immediate transitions are “dissolved” in the total transition rates between tangible states when vanishing states are eliminated from SMCs while reducing them to CTMCs. Therefore, to make the definition of fluid bisimulation less intricate and complex, we have decided to consider only LFSPNs with labeled CTSPNs as their discrete part. Then the underlying stochastic process of the discrete part of LFSPNs will be that of CTSPNs, i.e. CTMCs.

The novelty of the fluid bisimulation definition with respect to that of the Markovian bisimulations from [27, 54, 18, 16, 17, 19, 20, 21] is that, for each pair of bisimilar discrete markings of $N$ and $N^{\prime}$, we require coincidence of the fluid flow rates of the corresponding (i.e. related by a correspondence bijection) continuous places of $N$ and $N^{\prime}$ in these two discrete markings. Thus, fluid bisimulation equivalence takes into account functional activity, stochastic timing and fluid flow, like fluid trace equivalence does.

We first propose some helpful extensions of the rate functions for the discrete marking changes and for the fluid flow in continuous places. Let $N$ be an LFSPN and ${\cal H}\subseteq DRS(N)$. Then, for each $M\in DRS(N)$ and $a\in Act$, we write $M\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}{\cal H}$, where $\lambda=RM_{a}(M,{\cal H})$ is the overall rate to move from $M$ into the set of discrete markings ${\cal H}$ by action $a$, defined as

[TABLE]

We write $M\stackrel{{\scriptstyle a}}{{\rightarrow}}{\cal H}$ if $\exists\lambda\ M\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}{\cal H}$. Further, we write $M\rightarrow_{\lambda}{\cal H}$ if $\exists a\ M\stackrel{{\scriptstyle a}}{{\rightarrow}}{\cal H}$, where $\lambda=RM(M,{\cal H})$ is the overall rate to move from $M$ into the set of discrete markings ${\cal H}$ by any actions, defined as

[TABLE]

To construct a fluid bisimulation between LFSPNs $N$ and $N^{\prime}$, we should consider the “composite” set of their discrete markings $DRS(N)\cup DRS(N^{\prime})$, since we have to identify the rates to come from any two equivalent discrete markings into the same “composite” equivalence class (with respect to the fluid bisimulation). Note that, for $N\neq N^{\prime}$, transitions starting from the discrete markings of $DRS(N)$ (or $DRS(N^{\prime})$) always lead to those from the same set, since $DRS(N)\cap DRS(N^{\prime})=\emptyset$, and this allows us to “mix” the sets of discrete markings in the definition of fluid bisimulation.

Let $Pc_{N}=\{q\}$ and $Pc_{N^{\prime}}=\{q^{\prime}\}$. In this case the continuous place $q^{\prime}$ of $N$ corresponds to $q$ of $N$, according to a trivial correspondence bijection $\beta:Pc_{N}\rightarrow Pc_{N^{\prime}}$ such that $\beta(q)=q^{\prime}$. Then for $M\in DRS(N)$ (or for $M^{\prime}\in DRS(N^{\prime})$) we denote by $RP(M)$ (or by $RP(M^{\prime})$) the fluid level change rate for the continuous place $q$ (or for the corresponding one $q^{\prime}$), i.e. the argument discrete marking determines for which of the two continuous places, $q$ or $q^{\prime}$, the flow rate function $RP$ is taken.

Note that if $N$ and $N^{\prime}$ have more than one continuous place and there exists a correspondence bijection $\beta:Pc_{N}\rightarrow Pc_{N^{\prime}}$ then we should consider several flow rate functions $RP_{i}\ (1\leq i\leq l=|Pc_{N}|=|Pc_{N^{\prime}}|)$ in the same manner, i.e. each $RP_{i}$ is used for the pair of the corresponding continuous places $q_{i}\in Pc_{N}$ and $\beta(q_{i})=q_{i}^{\prime}\in Pc_{N^{\prime}}$. In other words, we require that the vectors $(RP_{1}(M),\ldots,RP_{l}(M))$ and $(RP_{1}(M^{\prime}),\ldots,RP_{l}(M^{\prime}))$ coincide for each pair of fluid bisimilar discrete markings $M$ and $M^{\prime}$ in such a case.

Definition 6.1

Let $N$ and $N^{\prime}$ be LFSPNs such that $Pc_{N}=\{q\},\ Pc_{N^{\prime}}=\{q^{\prime}\}$ and $q^{\prime}$ corresponds to $q$. An equivalence relation ${\cal R}\subseteq(DRS(N)\cup DRS(N^{\prime}))^{2}$ is a fluid bisimulation between $N$ and $N^{\prime}$, denoted by ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$, if:

$(M_{N},M_{N^{\prime}})\in{\cal R}$. 2. 2.

$(M_{1},M_{2})\in{\cal R}\ \Rightarrow\ RP(M_{1})=RP(M_{2}),\ \forall{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R},\ \forall a\in Act$**

[TABLE]

Two LFSPNs $N$ and $N^{\prime}$ are fluid bisimulation equivalent, denoted by $N\underline{\leftrightarrow}_{fl}N^{\prime}$, if $\exists{\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$.

Let ${\cal R}_{fl}(N,N^{\prime})=\bigcup\{{\cal R}\mid{\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}\}$ be the union of all fluid bisimulations between $N$ and $N^{\prime}$. The following proposition proves that ${\cal R}_{fl}(N,N^{\prime})$ is also an equivalence and ${\cal R}_{fl}(N,N^{\prime}):N\underline{\leftrightarrow}_{fl}N^{\prime}$.

Proposition 6.1

Let $N$ and $N^{\prime}$ be LFSPNs and $N\underline{\leftrightarrow}_{fl}N^{\prime}$. Then ${\cal R}_{fl}(N,N^{\prime})$ is the largest fluid bisimulation between $N$ and $N^{\prime}$.

Proof. Analogous to that of Proposition 8.2.1 from [54], which establishes the result for strong equivalence. $\sqcap\!\!\!\!\sqcup$

Let $N,N^{\prime}$ be LFSPNs with ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$ and ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$. We now present a number of remarks on the important equalities and helpful notations based on the rate functions $RM_{a},\ RM,\ RP$ and sojourn time characteristics $SJ,\ VAR$.

Remark 1. We have $\forall M_{1},M_{2}\in{\cal H}\ \forall\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}\ \forall a\in Act\ M_{1}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}\ \Leftrightarrow\ M_{2}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}$. Since the previous equality is valid for all $M_{1},M_{2}\in{\cal H}$, we can rewrite it as ${\cal H}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}$, where $\lambda=RM_{a}({\cal H},\widetilde{\cal H})=RM_{a}(M_{1},\widetilde{\cal H})=RM_{a}(M_{2},\widetilde{\cal H})=RM_{a}({\cal H}\cap DRS(N),\widetilde{\cal H})=RM_{a}({\cal H}\cap DRS(N^{\prime}),\widetilde{\cal H})$. Then we write ${\cal H}\stackrel{{\scriptstyle a}}{{\rightarrow}}\widetilde{\cal H}$ if $\exists{\lambda}\ {\cal H}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}$ and ${\cal H}\rightarrow\widetilde{\cal H}$ if $\exists a\ {\cal H}\stackrel{{\scriptstyle a}}{{\rightarrow}}\widetilde{\cal H}$.

Since the transitions from the discrete markings of $DRS(N)$ always lead to those from the same set, we have $\forall M\in DRS(N)\ \forall a\in Act\ RM_{a}(M,\widetilde{\cal H})=RM_{a}(M,\widetilde{\cal H}\cap DRS(N))$. Hence, $\forall M\in{\cal H}\cap DRS(N)\ \forall a\in Act\ RM_{a}({\cal H},\widetilde{\cal H})=RM_{a}(M,\widetilde{\cal H})=RM_{a}(M,\widetilde{\cal H}\cap DRS(N))=RM_{a}({\cal H}\cap DRS(N),\widetilde{\cal H}\cap DRS(N))$. The same is true for $DRS(N^{\prime})$. Thus, $\forall\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$

[TABLE]

Remark 2. We have $\forall M_{1},M_{2}\in{\cal H}\ \forall\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}\ RM(M_{1},\widetilde{\cal H})=\\ \sum_{\{t\mid\exists\widetilde{M}_{1}\in\widetilde{\cal H}\ M_{1}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{1}\}}\Omega_{N}(t,M_{1})=\sum_{a\in Act}\sum_{\{t\mid\exists\widetilde{M}_{1}\in\widetilde{\cal H}\ M_{1}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{1},\ L_{N}(t)=a\}}\Omega_{N}(t,M_{1})=\sum_{a\in Act}RM_{a}(M_{1},\widetilde{\cal H})=\\ \sum_{a\in Act}RM_{a}(M_{2},\widetilde{\cal H})=\sum_{a\in Act}\sum_{\{t\mid\exists\widetilde{M}_{2}\in\widetilde{\cal H}\ M_{2}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{2},\ L_{N}(t)=a\}}\Omega_{N}(t,M_{2})=\sum_{\{t\mid\exists\widetilde{M}_{2}\in\widetilde{\cal H}\ M_{2}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{2}\}}\Omega_{N}(t,M_{2})=\\ RM(M_{2},\widetilde{\cal H})$. Since the previous equality is valid for all $M_{1},M_{2}\in{\cal H}$, we can denote $RM({\cal H},\widetilde{\cal H})=RM(M_{1},\widetilde{\cal H})=RM(M_{2},\widetilde{\cal H})$. Then we write ${\cal H}\rightarrow_{\lambda}\widetilde{\cal H}$, where $\lambda=RM({\cal H},\widetilde{\cal H})=RM(M_{1},\widetilde{\cal H})=RM(M_{2},\widetilde{\cal H})$.

Since the transitions from the discrete markings of $DRS(N)$ always lead to those from the same set, we have $\forall M\in DRS(N)\ RM(M,\widetilde{\cal H})=RM(M,\widetilde{\cal H}\cap DRS(N))$. Hence, $\forall M\in{\cal H}\cap DRS(N)\ RM({\cal H},\widetilde{\cal H})=RM(M,\widetilde{\cal H})=RM(M,\widetilde{\cal H}\cap DRS(N))=RM({\cal H}\cap DRS(N),\widetilde{\cal H}\cap DRS(N))$. The same is true for $DRS(N^{\prime})$. Thus, $\forall\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$

[TABLE]

Remark 3. We have $\forall M_{1},M_{2}\in{\cal H}\ RP(M_{1})=RP(M_{2})$. Since the previous equality is valid for all $M_{1},M_{2}\in{\cal H}$, we can denote $RP({\cal H})=RP(M_{1})=RP(M_{2})$.

Since any argument discrete marking $M\in DRS(N)\cup DRS(N^{\prime})$ completely determines for which continuous place the flow rate function $RP(M)$ is taken (either for $q$ if $M\in DRS(N)$ or for $q^{\prime}$ if $M\in DRS(N^{\prime})$), we have $\forall M\in{\cal H}\cap DRS(N)\ RP({\cal H})=RP(M)=RP({\cal H}\cap DRS(N))$. The same is true for $DRS(N^{\prime})$. Thus,

[TABLE]

Remark 4. We have $\forall M_{1},M_{2}\in{\cal H}\ SJ(M_{1})=\frac{1}{\sum_{t\in Ena(M_{1})}\Omega_{N}(t,M_{1})}=\\ \frac{1}{\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{t\mid\exists\widetilde{M}_{1}\in\widetilde{\cal H}\ M_{1}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{1}\}}\Omega_{N}(t,M_{1})}=\frac{1}{\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(M_{1},\widetilde{\cal H})}=\\ \frac{1}{\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM({\cal H},\widetilde{\cal H})}=\frac{1}{\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(M_{2},\widetilde{\cal H})}=\\ \frac{1}{\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{t\mid\exists\widetilde{M}_{2}\in\widetilde{\cal H}\ M_{2}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{2}\}}\Omega_{N}(t,M_{2})}=\frac{1}{\sum_{t\in Ena(M_{2})}\Omega_{N}(t,M_{2})}=SJ(M_{2})$.

Since the previous equality is valid for all $M_{1},M_{2}\in{\cal H}$, we can denote $SJ_{\cal R}({\cal H})=SJ(M_{1})=SJ(M_{2})$.

Since any argument discrete marking $M\in DRS(N)\cup DRS(N^{\prime})$ completely determines, for which LFSPN the average sojourn time function $SJ(M)$ is considered (either for $N$ if $M\in DRS(N)$, or for $N^{\prime}$ if $M\in DRS(N^{\prime})$), we have $\forall M\in{\cal H}\cap DRS(N)\ SJ({\cal H})=SJ(M)=SJ({\cal H}\cap DRS(N))$. The same is true for $DRS(N^{\prime})$. Thus,

[TABLE]

Remark 5. We have $\forall M_{1},M_{2}\in{\cal H}\ VAR(M_{1})=\frac{1}{(\sum_{t\in Ena(M_{1})}\Omega_{N}(t,M_{1}))^{2}}=\\ \frac{1}{(\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{t\mid\exists\widetilde{M}_{1}\in\widetilde{\cal H}\ M_{1}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{1}\}}\Omega_{N}(t,M_{1}))^{2}}=\frac{1}{(\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(M_{1},\widetilde{\cal H}))^{2}}=\\ \frac{1}{(\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM({\cal H},\widetilde{\cal H}))^{2}}=\frac{1}{(\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(M_{2},\widetilde{\cal H}))^{2}}=\\ \frac{1}{(\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{t\mid\exists\widetilde{M}_{2}\in\widetilde{\cal H}\ M_{2}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}_{2}\}}\Omega_{N}(t,M_{2}))^{2}}=\frac{1}{(\sum_{t\in Ena(M_{2})}\Omega_{N}(t,M_{2}))^{2}}=VAR(M_{2})$.

Since the previous equality is valid for all $M_{1},M_{2}\in{\cal H}$, we can denote $VAR_{\cal R}({\cal H})=VAR(M_{1})=VAR(M_{2})$.

Since any argument discrete marking $M\in DRS(N)\cup DRS(N^{\prime})$ completely determines, for which LFSPN the sojourn time variance function $VAR(M)$ is considered (either for $N$ if $M\in DRS(N)$, or for $N^{\prime}$ if $M\in DRS(N^{\prime})$), we have $\forall M\in{\cal H}\cap DRS(N)\ VAR({\cal H})=VAR(M)=VAR({\cal H}\cap DRS(N))$. The same is true for $DRS(N^{\prime})$. Thus,

[TABLE]

Example 6.1

In Figure 7, the LFSPNs $N$ and $N^{\prime}$ are presented, such that $N\underline{\leftrightarrow}_{fl}N^{\prime}$. The only difference between the respective LFSPNs in Figure 1 and those in Figure 7 is that the transitions $t_{3}$ and $t_{4}^{\prime}$ are labeled with action $c$ in the former, instead of action $b$ in the latter.

Therefore, the following notions coincide for the respective LFSPNs in Figure 1 and those in Figure 7: the discrete reachability sets $DRS(N)$ and $DRS(N^{\prime})$, the discrete reachability graphs $DRG(N)$ and $DRG(N^{\prime})$, the underlying CTMCs $CTMC(N)$ and $CTMC(N^{\prime})$, the sojourn time average vectors $SJ$ and $SJ^{\prime}$ of $N$ and $N^{\prime}$, the variance vectors $VAR$ and $VAR^{\prime}$ of $N$ and $N^{\prime}$, the TRMs ${\bf Q}$ and ${\bf Q}^{\prime}$ for $CTMC(N)$ and $CTMC(N^{\prime})$, the TPMs ${\bf P}$ and ${\bf P}^{\prime}$ for $EDTMC(N)$ and $EDTMC(N^{\prime})$, the FRMs ${\bf R}$ and ${\bf R}^{\prime}$ for the SFMs of $N$ and $N^{\prime}$.

We have $DRS(N)/_{{\cal R}_{fl}(N)}=\{{\cal K}_{1},{\cal K}_{2}\}$, where ${\cal K}_{1}=\{M_{1}\},\ {\cal K}_{2}=\{M_{2}\}$, and $DRS(N^{\prime})/_{{\cal R}_{fl}(N^{\prime})}=\{{\cal K}_{1}^{\prime},{\cal K}_{2}^{\prime}\}$, where ${\cal K}_{1}^{\prime}=\{M_{1}^{\prime}\},\ {\cal K}_{2}^{\prime}=\{M_{2}^{\prime},M_{3}^{\prime}\}$.

We now intend to compare the introduced fluid equivalences to discover their interrelations. The following proposition demonstrates that fluid bisimulation equivalence implies fluid trace one.

Proposition 6.2

For LFSPNs $N$ and $N^{\prime}$ the following holds:

[TABLE]

Proof. Let ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime},\ {\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$ and $M_{1},M_{2}\in{\cal H}$. We have $RP(M_{1})=RP(M_{2})$ and $\forall\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}\ \forall a\in Act\ M_{1}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}\ \Leftrightarrow\ M_{2}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}$. Note that transitions from the discrete markings of $DRS(N)$ always lead to those from the same set, hence, $\forall M\in DRS(N)\ RM_{a}(M,\widetilde{\cal H})=RM_{a}(M,\widetilde{\cal H}\cap DRS(N))$. The same is true for $DRS(N^{\prime})$.

By Remark 1 from Section 6, we can write ${\cal H}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal H}$ and denote $\lambda=RM_{a}(M_{1},\widetilde{\cal H})=RM_{a}(M_{2},\widetilde{\cal H})=RM_{a}({\cal H},\widetilde{\cal H})=RM_{a}({\cal H}\cap DRS(N),\widetilde{\cal H}\cap DRS(N))=RM_{a}({\cal H}\cap DRS(N^{\prime}),\widetilde{\cal H}\cap DRS(N^{\prime}))$.

Further, by Remark 4 from Section 6, we can denote $SJ(M_{1})=SJ(M_{2})=SJ({\cal H})=SJ({\cal H}\cap DRS(N))=SJ({\cal H}\cap DRS(N^{\prime}))$.

At last, by Remark 3 from Section 6, we can denote $RP(M_{1})=RP(M_{2})=RP({\cal H})=RP({\cal H}\cap DRS(N))=RP({\cal H}\cap DRS(N^{\prime}))$.

Let $TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset$ and $\sigma=a_{1}\cdots a_{n}\in Act^{*},\ \varsigma=s_{0}\circ\cdots\circ s_{n}\in{\mathbb{R}}_{>0}^{*},\ \varrho=r_{0}\circ\cdots\circ r_{n}\in{\mathbb{R}}^{*}$. Taking into account the notes above and ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$, we have $SJ(M_{N})=SJ(M_{N^{\prime}})=s_{0},\ RP(M_{N})=RP(M_{N^{\prime}})=r_{0}$ and for all ${\cal H}_{1},\ldots,{\cal H}_{n}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$, such that $SJ({\cal H}_{i})=s_{i},\ RP({\cal H}_{i})=r_{i}\ (1\leq i\leq n)$, it holds $M_{N}\stackrel{{\scriptstyle a_{1}}}{{\rightarrow}}_{\lambda_{1}}{\cal H}_{1}\stackrel{{\scriptstyle a_{2}}}{{\rightarrow}}_{\lambda_{2}}\cdots\stackrel{{\scriptstyle a_{n}}}{{\rightarrow}}_{\lambda_{n}}{\cal H}_{n}\ \Leftrightarrow\ M_{N^{\prime}}\stackrel{{\scriptstyle a_{1}}}{{\rightarrow}}_{\lambda_{1}}{\cal H}_{1}\stackrel{{\scriptstyle a_{2}}}{{\rightarrow}}_{\lambda_{2}}\cdots\stackrel{{\scriptstyle a_{n}}}{{\rightarrow}}_{\lambda_{n}}{\cal H}_{n}$. Then we have $TranSeq(N^{\prime},\sigma,\varsigma,\varrho)\neq\emptyset$. Thus, $TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset$ implies $TranSeq(N^{\prime},\sigma,\varsigma,\varrho)\neq\emptyset$.

We now intend to prove that the sum of the transition rates products for all the paths starting in $M_{N}=M_{0}$ and going through the discrete markings from ${\cal H}_{1},\ldots,{\cal H}_{n}$ is equal to the product of $\lambda_{1},\ldots,\lambda_{n}$, which is essentially the transition rates product for the “composite” path starting in ${\cal H}_{0}=[M_{0}]_{\cal R}$ and going through the equivalence classes ${\cal H}_{1},\ldots,{\cal H}_{n}$ in $DRG(N)$:

[TABLE]

We prove this equality by induction on the “composite” path length $n$.

• •

$n=1$

$\sum_{\{t_{1}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1},\ L_{N}(t_{1})=a_{1},\ M_{1}\in{\cal H}_{1}\}}\Omega_{N}(t_{1},M_{0})=RM_{a_{1}}(M_{0},{\cal H}_{1})=RM_{a_{1}}({\cal H}_{0},{\cal H}_{1})$.

• •

$n\rightarrow n+1$

$\sum_{\{t_{1},\ldots,t_{n},t_{n+1}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}\stackrel{{\scriptstyle t_{n+1}}}{{\rightarrow}}M_{n+1},\ L_{N}(t_{i})=a_{i},\ M_{i}\in{\cal H}_{i}\ (1\leq i\leq n+1)\}}\prod_{i=1}^{n+1}\Omega_{N}(t_{i},M_{i-1})=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},\ M_{i}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\\ \sum_{\{t_{n+1}\mid M_{n}\stackrel{{\scriptstyle t_{n+1}}}{{\rightarrow}}M_{n+1},\ L_{N}(t_{n+1})=a_{n+1},\ M_{n}\in{\cal H}_{n},\ M_{n+1}\in{\cal H}_{n+1}\}}\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})\Omega_{N}(t_{n+1},M_{n})=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},\ M_{i}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\\ \left[\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})\sum_{\{t_{n+1}\mid M_{n}\stackrel{{\scriptstyle t_{n+1}}}{{\rightarrow}}M_{n+1},\ L_{N}(t_{n+1})=a_{n+1},\ M_{n}\in{\cal H}_{n},\ M_{n+1}\in{\cal H}_{n+1}\}}\Omega_{N}(t_{n+1},M_{n})\right]=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},\ M_{i}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})RM_{a_{n+1}}(M_{n},{\cal H}_{n+1})=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},\ M_{i}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})RM_{a_{n+1}}({\cal H}_{n},{\cal H}_{n+1})=\\ RM_{a_{n+1}}({\cal H}_{n},{\cal H}_{n+1})\sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},\ M_{i}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})=\\ RM_{a_{n+1}}({\cal H}_{n},{\cal H}_{n+1})\prod_{i=1}^{n}RM_{a_{i}}({\cal H}_{i-1},{\cal H}_{i})=\prod_{i=1}^{n+1}RM_{a_{i}}({\cal H}_{i-1},{\cal H}_{i})$.

Note that the equality that we have just proved can also be applied to $N^{\prime}$.

One can see that the summation over all $(\sigma,\varsigma,\varrho)$-selected transition sequences is the same as the summation over all accordingly selected equivalence classes: $\sum_{t_{1}\cdots t_{n}\in TranSeq(N,\sigma,\varsigma,\varrho)}\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},\ SJ(M_{i})=s_{i},\ RP(M_{j})=r_{i}\ (1\leq i\leq n)\}}\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})=\\ \sum_{\{{\cal H}_{1},\ldots,{\cal H}_{n}\mid SJ({\cal H}_{i})=s_{i},RP({\cal H}_{i})=r_{i}\ (1\leq i\leq n)\}}\!\!\sum_{\{t_{1},\ldots,t_{n}\mid M_{N}=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{i})=a_{i},M_{i}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\!\!\prod_{i=1}^{n}\Omega_{N}(t_{i},M_{i-1})\!\!=\\ \sum_{\{{\cal H}_{1},\ldots,{\cal H}_{n}\mid SJ({\cal H}_{i})=s_{i},\ RP({\cal H}_{i})=r_{i}\ (1\leq i\leq n)\}}\prod_{i=1}^{n}RM_{a_{i}}({\cal H}_{i-1},{\cal H}_{i})=\\ \sum_{\{{\cal H}_{1},\ldots,{\cal H}_{n}\mid SJ({\cal H}_{i})=s_{i},RP({\cal H}_{i})=r_{i}\ (1\leq i\leq n)\}}\!\!\sum_{\{t_{1}^{\prime},\ldots,t_{n}^{\prime}\mid M_{N^{\prime}}=M_{0}^{\prime}\stackrel{{\scriptstyle t_{1}^{\prime}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}^{\prime}}}{{\rightarrow}}M_{n}^{\prime},\ L_{N}(t_{i}^{\prime})=a_{i},M_{i}^{\prime}\in{\cal H}_{i}\ (1\leq i\leq n)\}}\!\!\!\!\prod_{i=1}^{n}\Omega_{N^{\prime}}(t_{i}^{\prime},M_{i-1}^{\prime})\!\!=\\ \sum_{\{t_{1}^{\prime},\ldots,t_{n}^{\prime}\mid M_{N^{\prime}}=M_{0}^{\prime}\stackrel{{\scriptstyle t_{1}^{\prime}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}^{\prime}}}{{\rightarrow}}M_{n}^{\prime},\ L_{N^{\prime}}(t_{i}^{\prime})=a_{i},\ SJ(M_{i}^{\prime})=s_{i},\ RP(M_{j}^{\prime})=r_{i}\ (1\leq i\leq n)\}}\prod_{i=1}^{n}\Omega_{N^{\prime}}(t_{i}^{\prime},M_{i-1}^{\prime})=\\ \sum_{t_{1}^{\prime}\cdots t_{n}^{\prime}\in TranSeq(N^{\prime},\sigma,\varsigma,\varrho)}\prod_{i=1}^{n}\Omega_{N}(t_{i}^{\prime},M_{i-1}^{\prime})$. By the remark before Definition 5.4, the probabilities to execute $(\sigma,\varsigma,\varrho)$-selected transition sequences in $N$ and $N^{\prime}$ coincide.

We conclude that for all triples $(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$, it holds that $TranSeq(N,\sigma,\varsigma,\varrho)\neq\emptyset$ implies $TranSeq(N^{\prime},\sigma,\varsigma,\varrho)\neq\emptyset$ and the execution probabilities of $(\sigma,\varsigma,\varrho)$ in $N$ and $N^{\prime}$ are equal. The reverse implication is proved by symmetry of fluid bisimulation. $\sqcap\!\!\!\!\sqcup$

The following theorem compares discriminating power of the introduced fluid equivalences.

Theorem 6.1

For LFSPNs $N$ and $N^{\prime}$ the following strict implication holds that is also depicted in Figure 8:

[TABLE]

Proof. Let us check the validity of the implication.

• •

The implication $\underline{\leftrightarrow}_{fl}\rightarrow\equiv_{fl}$ is valid by Proposition 6.2.

Let us see that the implication is strict, i.e. the reverse one does not work, by the following counterexample.

• •

In Figure 1, $N\equiv_{fl}N^{\prime}$, but $N\underline{\leftrightarrow}\!\!\!\!/\ _{fl}N^{\prime}$, since only in the LFSPN $N^{\prime}$ an action $a$ can be executed so (by firing the transition $t_{2}^{\prime}$) that no action $b$ can occur afterwards. $\sqcap\!\!\!\!\sqcup$

7 Reduction of the behaviour

Fluid bisimulation equivalence can be used to reduce the discrete reachability graphs and underlying CTMCs of LFSPNs. Reductions of graph-based models, like transition systems (whose instances are reachability graphs and CTMCs), result in those with less states (the graph nodes). The goal of the reduction is to decrease the number of states in the semantic representation of the modeled system while preserving its important qualitative and quantitative properties. Thus, the reduction allows one to simplify the behavioural and performance analysis of systems.

An autobisimulation is a bisimulation between an LFSPN and itself. Let $N$ be an LFSPN with ${\cal R}:N\underline{\leftrightarrow}_{fl}N$ and ${\cal K}\in DRS(N)/_{\cal R}$.

Then Remarks 2, 4 and 5 from Section 6 allow us to present the following definitions.

The average sojourn time in the equivalence class (with respect to ${\cal R}$) of discrete markings ${\cal K}$ is

[TABLE]

The average sojourn time vector for the equivalence classes (with respect to ${\cal R}$) of discrete markings of $N$, denoted by $SJ_{\cal R}$, has the elements $SJ_{\cal R}({\cal K}),\ {\cal K}\in DRS(N)/_{\cal R}$.

The sojourn time variance in the equivalence class (with respect to ${\cal R}$) of discrete markings ${\cal K}$ is

[TABLE]

The sojourn time variance vector for the equivalence classes (with respect to ${\cal R}$) of discrete markings of $N$, denoted by $VAR_{\cal R}$, has the elements $VAR_{\cal R}({\cal K}),\ {\cal K}\in DRS(N)/_{\cal R}$.

Let ${\cal R}_{fl}(N)=\bigcup\{{\cal R}\mid{\cal R}:N\underline{\leftrightarrow}_{fl}N\}$ be the union of all fluid autobisimulations on $N$. By Proposition 6.1, ${\cal R}_{fl}(N)$ is the largest fluid autobisimulation on $N$. Based on the equivalence classes with respect to ${\cal R}_{fl}(N)$, the quotient (by $\underline{\leftrightarrow}_{fl}$) discrete reachability graphs and quotient (by $\underline{\leftrightarrow}_{fl}$) underlying CTMCs of LFSPNs can be defined. The mentioned equivalence classes become the quotient states. The average and variance for the sojourn time in a quotient state are those in the corresponding equivalence class, respectively. Every quotient transition between two such composite states represents all transitions (having the same action label in case of the discrete reachability graph quotient) from the first state to the second one.

Definition 7.1

Let $N$ be an LFSPN. The quotient (by $\underline{\leftrightarrow}_{fl}$) discrete reachability graph of $N$ is a labeled transition system $DRG_{\underline{\leftrightarrow}_{fl}}(N)=(S_{\underline{\leftrightarrow}_{fl}},{\cal L}_{\underline{\leftrightarrow}_{fl}},{\cal T}_{\underline{\leftrightarrow}_{fl}},s_{\underline{\leftrightarrow}_{fl}})$, where

• •

$S_{\underline{\leftrightarrow}_{fl}}=DRS(N)/_{{\cal R}_{fl}(N)}$;

• •

${\cal L}_{\underline{\leftrightarrow}_{fl}}=Act\times{\mathbb{R}}_{>0}$;

• •

${\cal T}_{\underline{\leftrightarrow}_{fl}}=\{({\cal K},(a,RM_{a}({\cal K},\widetilde{\cal K})),\widetilde{\cal K})\mid{\cal K},\widetilde{\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)},\ {\cal K}\stackrel{{\scriptstyle a}}{{\rightarrow}}\widetilde{\cal K}\}$;

• •

$s_{\underline{\leftrightarrow}_{fl}}=[M_{N}]_{{\cal R}_{fl}(N)}$.

The transition $({\cal K},(a,\lambda),\widetilde{\cal K})\in{\cal T}_{\underline{\leftrightarrow}_{fl}}$ will be written as ${\cal K}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}\widetilde{\cal K}$.

Let $\simeq$ denote isomorphism between the quotient discrete reachability graphs that binds their initial states.

The quotient (by $\underline{\leftrightarrow}_{fl}$) average sojourn time vector of $N$ is defined as $SJ_{\underline{\leftrightarrow}_{fl}}=SJ_{{\cal R}_{fl}(N)}$. The quotient (by $\underline{\leftrightarrow}_{fl}$) sojourn time variance vector of $N$ is defined as $VAR_{\underline{\leftrightarrow}_{fl}}=VAR_{{\cal R}_{fl}(N)}$.

Definition 7.2

*Let $N$ be an LFSPN. The quotient (by $\underline{\leftrightarrow}_{fl}$) underlying CTMC of $N$, denoted by

$CTMC_{\underline{\leftrightarrow}_{fl}}(N)$, has the state space $DRS(N)/_{{\cal R}_{fl}(N)}$, the initial state $[M_{N}]_{{\cal R}_{fl}(N)}$ and the transitions ${\cal K}\rightarrow_{\lambda}\widetilde{\cal K}$ if ${\cal K}\rightarrow\widetilde{\cal K}$, where $\lambda=RM({\cal K},\widetilde{\cal K})$.*

The steady-state PMF $\varphi_{\underline{\leftrightarrow}_{fl}}$ for $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ is defined like the corresponding notion $\varphi$ for $CTMC(N)$.

The quotients of both discrete reachability graphs and underlying CTMCs are the minimal reductions of the mentioned objects modulo fluid bisimulation. The quotients can be used to simplify analysis of system properties which are preserved by $\underline{\leftrightarrow}_{fl}$, since less states should be examined for it. Such a reduction method resembles that from [7] based on place bisimulation equivalence for Petri nets, excepting that the former method merges states, while the latter one merges places.

Let $N$ be an LFSPN. We shall now demonstrate how to construct the quotients (by $\underline{\leftrightarrow}_{fl}$) of the TRM for $CTMC(N)$, FRM for the associated SFM of $N$, average sojourn time vector and sojourn time variance vector of $N$, using special collector and distributor matrices. The quotient TRMs and FRMs will be later applied to describe the quotient associated SFMs of LFSPNs. Let $DRS(N)=\{M_{1},\ldots,M_{n}\}$ and $DRS(N)/_{{\cal R}_{fl}(N)}=\{{\cal K}_{1},\ldots,{\cal K}_{l}\}$.

The elements $({\cal Q}_{\underline{\leftrightarrow}_{fl}})_{rs}\ (1\leq r,s\leq l)$ of the TRM ${\bf Q}_{\underline{\leftrightarrow}_{fl}}$ for $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ are defined as

[TABLE]

Like it has been done for strong performance bisimulation on labeled CTSPNs in [27], the $l\times l$ TRM ${\bf Q}_{\underline{\leftrightarrow}_{fl}}$ for $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ can be constructed from the $n\times n$ TRM ${\bf Q}$ for $CTMC(N)$ using the $n\times l$ collector matrix ${\bf V}$ for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$ and the $l\times n$ distributor matrix ${\bf W}$ for ${\bf V}$. Then ${\bf W}$ should be a non-negative matrix (i.e. all its elements must be non-negative) with the elements of each its row summed to one, such that ${\bf W}{\bf V}={\bf I}$, where ${\bf I}$ is the identity matrix of order $l$, i.e. ${\bf W}$ is a left-inverse matrix for ${\bf V}$. It is known that for each collector matrix there is at least one distributor matrix, in particular, the matrix obtained by transposing ${\bf V}$ and subsequent normalizing its rows, to guarantee that the elements of each row of the transposed matrix are summed to one. We now present the formal definitions.

The elements ${\cal V}_{ir}\ (1\leq i\leq n,\ 1\leq r\leq l)$ of the collector matrix ${\bf V}$ for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$ are defined as

[TABLE]

Thus, all the elements of ${\cal V}$ are non-negative, as required. The row elements of ${\cal V}$ are summed to one, since for each $M_{i}\ (1\leq i\leq n)$ there exists exactly one ${\cal K}_{r}\ (1\leq r\leq l)$ such that $M_{i}\in{\cal K}_{r}$. Hence,

[TABLE]

where ${\bf 1}$ on the left side is the row vector of $l$ values $1$ while ${\bf 1}$ on the right side is the row vector of $n$ values $1$.

For a vector $v=(v_{1},\ldots,v_{l})$, let $Diag(v)$ be a diagonal matrix with the elements $Diag_{rs}(v)\ (1\leq r,s\leq l)$ defined as

[TABLE]

The distributor matrix ${\bf W}$ for the collector matrix ${\bf V}$ is defined as

[TABLE]

where ${\bf 1}$ is the row vector of $n$ values $1$. One can check that ${\bf W}{\bf V}={\bf I}$, where ${\bf I}$ is the identity matrix of order $l$.

The elements $({\cal Q}{\cal V})_{is}\ (1\leq i\leq n,\ 1\leq s\leq l)$ of the matrix ${\bf Q}{\bf V}$ are

[TABLE]

As we know, for each $M_{i}\ (1\leq i\leq n)$ there exists exactly one ${\cal K}_{r}\ (1\leq r\leq l)$ such that $M_{i}\in{\cal K}_{r}$. By Remark 2 from Section 6, for all $M_{i}\in{\cal K}_{r}$ we have $RM({\cal K}_{r},{\cal K}_{s})=RM(M_{i},{\cal K}_{s})\ (1\leq i\leq n,\ 1\leq r,s\leq l)$. Then the elements $({\cal V}{\cal Q}_{\underline{\leftrightarrow}_{fl}})_{is}\ (1\leq i\leq n,\ 1\leq s\leq l)$ of the matrix ${\bf V}{\bf Q}_{\underline{\leftrightarrow}_{fl}}$ are

[TABLE]

Therefore, we have

[TABLE]

The elements $({\cal R}_{\underline{\leftrightarrow}_{fl}})_{rs}\ (1\leq r,s\leq l)$ of the FRM ${\bf R}_{\underline{\leftrightarrow}_{fl}}$ of the quotient (by $\underline{\leftrightarrow}_{fl}$) SFM of $N$ for the continuous place $q$ are defined as

[TABLE]

Let ${\bf R}$ be the FRM of the SFM of $N$ for the continuous place $q$. The elements $({\cal R}{\cal V})_{is}\ (1\leq i\leq n,\ 1\leq s\leq l)$ of the matrix ${\bf R}{\bf V}$ are

[TABLE]

By Remark 2 from Section 6, for all $M_{i}\in{\cal K}_{s}$ we have $RP({\cal K}_{s})=RP(M_{i})\ (1\leq i\leq n,\ 1\leq s\leq l)$. Then the elements $({\cal V}{\cal R}_{\underline{\leftrightarrow}_{fl}})_{is}\ (1\leq i\leq n,\ 1\leq s\leq l)$ of the matrix ${\bf V}{\bf R}_{\underline{\leftrightarrow}_{fl}}$ are

[TABLE]

Therefore, we also have

[TABLE]

Let us consider the matrices $Diag(SJ)$ and $Diag(SJ_{\underline{\leftrightarrow}_{fl}})$. By analogy with the proven above for ${\bf R}$ and ${\bf R}_{\underline{\leftrightarrow}_{fl}}$, we can deduce $Diag(SJ){\bf V}={\bf V}Diag(SJ_{\underline{\leftrightarrow}_{fl}})$ and ${\bf W}Diag(SJ){\bf V}=Diag(SJ_{\underline{\leftrightarrow}_{fl}})$. Therefore, we have

[TABLE]

where ${\bf 1}$ is the row vector of $l$ values $1$. In a similar way, we obtain

[TABLE]

where ${\bf 1}$ is the row vector of $l$ values $1$.

Example 7.1

Consider the LFSPNs $N$ and $N^{\prime}$ from Figure 7, for which it holds $N\underline{\leftrightarrow}_{fl}N^{\prime}$.

In Figure 9, the quotient discrete reachability graphs $DRG_{\underline{\leftrightarrow}_{fl}}(N)$ and $DRG_{\underline{\leftrightarrow}_{fl}}(N^{\prime})$ are depicted, for which we have $DRG_{\underline{\leftrightarrow}_{fl}}(N)\simeq DRG_{\underline{\leftrightarrow}_{fl}}(N^{\prime})$. In Figure 10, the quotient underlying CTMCs $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ and $CTMC_{\underline{\leftrightarrow}_{fl}}(N^{\prime})$ are drawn, for which it holds $CTMC_{\underline{\leftrightarrow}_{fl}}(N)\simeq CTMC_{\underline{\leftrightarrow}_{fl}}(N^{\prime})\simeq CTMC(N)$.

We have ${\bf Q}_{\underline{\leftrightarrow}_{fl}}={\bf Q}_{\underline{\leftrightarrow}_{fl}}^{\prime}={\bf Q},\ {\bf R}_{\underline{\leftrightarrow}_{fl}}={\bf R}_{\underline{\leftrightarrow}_{fl}}^{\prime}={\bf R}$ and $SJ_{\underline{\leftrightarrow}_{fl}}=SJ_{\underline{\leftrightarrow}_{fl}}^{\prime}=SJ,\ VAR_{\underline{\leftrightarrow}_{fl}}=VAR_{\underline{\leftrightarrow}_{fl}}^{\prime}=VAR$.

The collector matrix ${\bf V}$ for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$ and the distributor matrix ${\bf W}$ for ${\bf V}$ are

[TABLE]

Then it is easy to check that

[TABLE]

Hence, it holds that

[TABLE]

[TABLE]

8 Logical characterization

In this section, a logical characterization of fluid trace and bisimulation equivalences is accomplished via formulas of the novel fluid modal logics. The results obtained could be interpreted as an operational characterization of the corresponding logical equivalences.

8.1 Logic $HML_{flt}$

The modal logic $HML_{NPMTr}$ has been introduced in [18, 16, 19] (called $HML_{MTr}$ in [18, 16]) on (sequential) and concurrent Markovian process calculi SMPC (called MPC in [18, 19]) and CMPC for logical interpretation of Markovian trace equivalence. $HML_{NPMTr}$ is based on the logic HML [53], to which a new interpretation function has been added that takes as its arguments a process state and a sum or a sequence of the average sojourn times.

We now propose a novel fluid modal logic $HML_{flt}$ for the characterization of fluid trace equivalence. For this, we extend the interpretation function of $HML_{NPMTr}$ with an additional argument, which is the sequence of the potential fluid flow rates for the single continuous place of an LFSPN (remember that in the standard definition of fluid trace equivalence we compare only LFSPNs, each having exactly one continuous place).

Note that Markovian trace equivalence and the corresponding interpretation function for $HML_{MTr}$ in [18] are defined by summing up the average sojourn times in the process states. In our definition of fluid trace equivalence, we consider sequences of the average sojourn times in the discrete markings of LFSPNs. Hence, our fluid extension of $HML_{NPMTr}$ is based rather on the definitions from [16, 19], where the latter approach (i.e. the sequences instead of sums) has been presented.

Definition 8.1

Let $\top$ denote the truth and $a\in Act$. A formula of $HML_{flt}$ is defined as follows:

[TABLE]

${\bf HML}_{flt}$ denotes the set of all formulas of the logic $HML_{flt}$.

Definition 8.2

Let $N$ be an LFSPN and $M\in DRS(N)$. The interpretation function $[\![\,]\!]_{flt}:DRS(N)\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}\rightarrow{\bf HML}_{flt}$ is defined as follows:

[\![\top]\!]_{flt}(M,\varsigma,\varrho)=\left\{\begin{array}[]{ll}0,&(\varsigma\neq SJ(M))\vee(\varrho\neq RP(M));\\ 1,&(\varsigma=SJ(M))\wedge(\varrho=RP(M));\end{array}\right.** 2. 2.

[\![\langle a\rangle\Phi]\!]_{flt}(M,\varsigma,\varrho)=\left\{\begin{array}[]{ll}0,&(\varsigma=\varepsilon)\vee(\varrho=\varepsilon)\vee\\ &((\varsigma=s\circ\hat{\varsigma})\wedge(SJ(M)\neq s))\vee\\ &((\varrho=r\circ\hat{\varrho})\wedge(RP(M)\neq r));\\ \sum_{\{t\mid M\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M},\ L_{N}(t)=a\}}PT(t,M)[\![\Phi]\!]_{flt}(\widetilde{M},\hat{\varsigma},\hat{\varrho}),&(\varsigma=s\circ\hat{\varsigma})\wedge(SJ(M)=s)\wedge\\ &(\varrho=r\circ\hat{\varrho})\wedge(RP(M)=r).\end{array}\right.**

Note that the item $1$ in the definition above describes the situation when only the empty transition sequence should start in the discrete marking $M$ to reach the state (which is $M$ itself), described by the identically true formula. Since we have just a single (mentioned) true state, it remains to check that second and third arguments of the interpretation function are the sequences of length one, as well as that they are equal to the average sojourn time and fluid flow rate in $M$, respectively.

Definition 8.3

Let $N$ be an LFSPN. Then we define $[\![\Phi]\!]_{flt}(N,\varsigma,\varrho)=[\![\Phi]\!]_{flt}(M_{N},\varsigma,\varrho)$. Two LFSPNs $N$ and $N^{\prime}$ are logically equivalent in $HML_{flt}$, denoted by $N=_{HML_{flt}}N^{\prime}$, if $\forall\Phi\in{\bf HML}_{flt}\ \forall\varsigma\in{\mathbb{R}}_{>0}^{*}\ \forall\varrho\in{\mathbb{R}}^{*}\ [\![\Phi]\!]_{flt}(N,\varsigma,\varrho)=[\![\Phi]\!]_{flt}(N^{\prime},\varsigma,\varrho)$.

Let $N$ be an LFSPN and $M\in DRS(N),\ a\in Act$. The set of discrete markings reached from $M$ by execution of action $a$, called the image set, is defined as $Image(M,a)=\{\widetilde{M}\mid M\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M},\ L_{N}(t)=a\}$. An LFSPN $N$ is an image-finite one, if $\forall M\in DRS(N)\ \forall a\in Act\ |Image(M,a)|<\infty$.

In order to get the intended logical characterization, we need in some auxiliary definitions considering the transition sequences starting not just in the initial discrete marking of an LFSPN, but in any reachable one.

Let $N$ be an LFSPN and $M\in DRS(N)$. The set of all (finite) transition sequences in $N$ starting in the discrete marking $M$ is defined as

[TABLE]

Let $\vartheta=t_{1}\cdots t_{n}\in TranSeq(N,M)$ and $M=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n}$. The probability to execute the transition sequence $\vartheta$ is

[TABLE]

For $\vartheta=\varepsilon$ we define $PT(\varepsilon)=1$.

Let $(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$. The set of $(\sigma,\varsigma,\varrho)$-selected (finite) transition sequences in $N$ starting in the discrete marking $M$ is defined as

[TABLE]

The (cumulative) probability to execute $(\sigma,\varsigma,\varrho)$-selected transition sequences starting in the discrete marking $M$ is

[TABLE]

The following lemma provides a recursive definition of $PT(M,\sigma,\varsigma,\varrho)$ that will be used later in the proofs.

Lemma 8.1

Let $N$ be an LFSPN and $M\in DRS(N)$. Then for all $(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$ such that $\sigma=a\cdot\hat{\sigma},\ \varsigma=s\circ\hat{\varsigma},\ \varrho=r\circ\hat{\varrho}$, where $a\in Act,\ s\in{\mathbb{R}}_{>0},\ r\in{\mathbb{R}}$, we have

[TABLE]

Proof. It holds that $PT(M,\sigma,\varsigma,\varrho)=\sum_{\vartheta\in TranSeq(N,M,\sigma,\varsigma,\varrho)}PT(\vartheta)=\\ \sum_{\{t_{1},\ldots,t_{n}\mid M=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{1}\cdots t_{n})=\sigma,\ SJ(M_{0}\cdots M_{n})=\varsigma,\ RP(M_{0}\cdots M_{n})=\varrho\}}\prod_{i=1}^{n}PT(t_{i},M_{i-1})=\\ \sum_{\{t_{1}\mid M=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1},\ L_{N}(t_{1})=a,\ SJ(M_{0})=s,\ RP(M_{0})=r\}}\\ \sum_{\{t_{2},\ldots,t_{n}\mid M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}M_{2}\stackrel{{\scriptstyle t_{3}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{2}\cdots t_{n})=\hat{\sigma},\ SJ(M_{1}\cdots M_{n})=\hat{\varsigma},\ RP(M_{1}\cdots M_{n})=\hat{\varrho}\}}PT(t_{1},M_{0})\prod_{i=2}^{n}PT(t_{i},M_{i-1})=\\ \sum_{\{t_{1}\mid M=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1},\ L_{N}(t_{1})=a,\ SJ(M_{0})=s,\ RP(M_{0})=r\}}\\ PT(t_{1},M_{0})\left(\sum_{\{t_{2},\ldots,t_{n}\mid M_{1}\stackrel{{\scriptstyle t_{2}}}{{\rightarrow}}M_{2}\stackrel{{\scriptstyle t_{3}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle t_{n}}}{{\rightarrow}}M_{n},\ L_{N}(t_{2}\cdots t_{n})=\hat{\sigma},\ SJ(M_{1}\cdots M_{n})=\hat{\varsigma},\ RP(M_{1}\cdots M_{n})=\hat{\varrho}\}}\prod_{i=2}^{n}PT(t_{i},M_{i-1})\right)=\\ \sum_{\{t_{1}\mid M=M_{0}\stackrel{{\scriptstyle t_{1}}}{{\rightarrow}}M_{1},\ L_{N}(t_{1})=a,\ SJ(M_{0})=s,\ RP(M_{0})=r\}}PT(t_{1},M_{0})PT(M_{1},\hat{\sigma},\hat{\varsigma},\hat{\varrho})$. Let us now $t=t_{1}$ and $\widetilde{M}=M_{1}$. $\sqcap\!\!\!\!\sqcup$

The following propositions demonstrate that there exists a bijective correspondence between fluid stochastic traces of LFSPNs and formulas of ${\bf HML}_{flt}$, by proving that the probabilities of the triples $(\sigma,\varsigma,\varrho)\in Act^{*}\times{\mathbb{R}}_{>0}^{*}\times{\mathbb{R}}^{*}$ coincide in the net and logical frameworks.

Proposition 8.1

Let $N$ be an image-finite LFSPN. Then for each $\sigma\in Act^{*}$ there exists $\Phi_{\sigma}\in{\bf HML}_{flt}$ such that $\forall M\in DRS(N)\ \forall\varsigma\in{\mathbb{R}}_{>0}^{*}\ \forall\varrho\in{\mathbb{R}}^{*}$

[TABLE]

Proof. We prove by induction on the length $n$ of the action sequence $\sigma$.

• •

$n=0$

We have $|\sigma|=0$, hence, $\sigma=\varepsilon$. In this case, we take $\Phi_{\sigma}=\top$. Let $M\in DRS(N),\ \varsigma\in{\mathbb{R}}_{>0}^{*},\ \varrho\in{\mathbb{R}}^{*}$.

If $(\varsigma\neq SJ(M))\vee(\varrho\neq RP(M))$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)=\emptyset$ and

[TABLE]

Otherwise, if $(\varsigma=SJ(M))\wedge(\varrho=RP(M))$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)=\{\varepsilon\}$ and

[TABLE]

• •

$n\rightarrow n+1$

We have $|\sigma|=n+1$, hence, $\sigma=a\cdot\hat{\sigma}$, where $a\in Act$ and $|\hat{\sigma}|=n$. In this case, we take $\Phi_{\sigma}=\langle a\rangle\Phi_{\hat{\sigma}}$, where the indiction hypothesis holds for $\hat{\sigma}$ and $\Phi_{\hat{\sigma}}$. Let $M\in DRS(N),\ \varsigma\in{\mathbb{R}}_{>0}^{*},\ \varrho\in{\mathbb{R}}^{*}$.

If no transition labeled with action $a$ is enabled in $M$ or $(\varsigma=\varepsilon)\vee(\varrho=\varepsilon)\vee((\varsigma=s\circ\hat{\varsigma})\wedge(SJ(M)\neq s))\vee((\varrho=r\circ\hat{\varrho})\wedge(RP(M)\neq r))$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)=\emptyset$ and

[TABLE]

Otherwise, if transitions labeled with action $a$ are enabled in $M$ and $(\varsigma=s\circ\hat{\varsigma})\wedge(SJ(M)=s)\wedge(\varrho=r\circ\hat{\varrho})\wedge(RP(M)=r)$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)\neq\emptyset$ and

[TABLE]

as well as

[TABLE]

By the induction hypothesis, for all discrete markings $\widetilde{M}$ reachable from $M$ by firing transitions labeled with action $a$ we have

[TABLE]

thus, we have proven. $\sqcap\!\!\!\!\sqcup$

Proposition 8.2

Let $N$ be an image-finite LFSPN. Then for each $\Phi\in{\bf HML}_{flt}$ there exists $\sigma_{\Phi}\in Act^{*}$ such that $\forall M\in DRS(N)\ \forall\varsigma\in{\mathbb{R}}_{>0}^{*}\ \forall\varrho\in{\mathbb{R}}^{*}$

[TABLE]

Proof. We prove by induction on the syntactical structure of the logical formula $\Phi$.

• •

$\Phi=\top$

In this case, we take $\sigma_{\Phi}=\varepsilon$. Let $M\in DRS(N),\ \varsigma\in{\mathbb{R}}_{>0}^{*},\ \varrho\in{\mathbb{R}}^{*}$.

If $(\varsigma\neq SJ(M))\vee(\varrho\neq RP(M))$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)=\emptyset$ and

[TABLE]

Otherwise, if $(\varsigma=SJ(M))\wedge(\varrho=RP(M))$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)=\{\varepsilon\}$ and

[TABLE]

• •

$\Phi=\langle a\rangle\Phi$

In this case, we take $\sigma_{\Phi}=a\cdot\sigma_{\widehat{\Phi}}$, where the indiction hypothesis holds for $\widehat{\Phi}$ and $\sigma_{\widehat{\Phi}}$. Let $M\in DRS(N),\ \varsigma\in{\mathbb{R}}_{>0}^{*},\ \varrho\in{\mathbb{R}}^{*}$.

If no transition labeled with action $a$ is enabled in $M$ or $(\varsigma=\varepsilon)\vee(\varrho=\varepsilon)\vee((\varsigma=s\circ\hat{\varsigma})\wedge(SJ(M)\neq s))\vee((\varrho=r\circ\hat{\varrho})\wedge(RP(M)\neq r))$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)=\emptyset$ and

[TABLE]

Otherwise, if transitions labeled with action $a$ are enabled in $M$ and $(\varsigma=s\circ\hat{\varsigma})\wedge(SJ(M)=s)\wedge(\varrho=r\circ\hat{\varrho})\wedge(RP(M)=r)$ then $TranSeq(N,M,\sigma,\varsigma,\varrho)\neq\emptyset$ and

[TABLE]

as well as

[TABLE]

By the induction hypothesis, for all discrete markings $\widetilde{M}$ reachable from $M$ by firing transitions labeled with action $a$ we have

[TABLE]

thus, we have proven. $\sqcap\!\!\!\!\sqcup$

Theorem 8.1

For image-finite LFSPNs $N$ and $N^{\prime}$

[TABLE]

Proof. The result follows from Proposition 8.1 and Proposition 8.2, which establish a bijective correspondence between fluid stochastic traces of LFSPNs and formulas of ${\bf HML}_{flt}$. $\sqcap\!\!\!\!\sqcup$

Thus, in the trace semantics, we obtained a logical characterization of the fluid behavioural equivalence or, symmetrically, an operational characterization of the fluid modal logic equivalence.

Example 8.1

Consider the LFSPNs $N$ and $N^{\prime}$ from Figure 1, for which it holds $N\equiv_{fl}N^{\prime}$, hence, $N=_{HML_{flt}}N^{\prime}$. In particular, for $\Phi=\langle\{a\}\rangle\langle\{b\}\rangle\top$ we have $\sigma_{\Phi}=a\cdot b$ and $[\![\Phi]\!]_{flt}(M_{N},\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1)=PT(t_{1}t_{2})=1\cdot\frac{1}{2}=\frac{1}{2}=1\cdot\frac{1}{2}=PT(t_{1}^{\prime}t_{3}^{\prime})=[\![\Phi]\!]_{flt}(M_{N^{\prime}},\frac{1}{2}\circ\frac{1}{2}\circ\frac{1}{2},1\circ(-2)\circ 1)$.

8.2 Logic $HML_{flb}$

The modal logic $HML_{MB}$ has been introduced in [16, 19] on sequential and concurrent Markovian process calculi SMPC (called MPC in [19]) and CPMC for logical interpretation of Markovian bisimulation equivalence. $HML_{MB}$ is based on the logic HML [53], in which the diamond operator was decorated with the rate lower bound. Hence, $HML_{MB}$ can be also seen as a modification of the logic $PML$ [60], where the probability lower bound that decorates the diamond operator was replaced with the rate lower bound.

We now propose a novel fluid modal logic $HML_{flb}$ for the characterization of fluid bisimulation equivalence. For this, we add to $HML_{MB}$ a new modality $\wr_{r}$, where $r\in{\mathbb{R}}$ is the potential fluid flow rate value for the single continuous place of an LFSPN (remember that in the standard definition of fluid bisimulation equivalence we compare only LFSPNs, each having exactly one continuous place). The formula $\wr_{r}$ is used to check whether the potential fluid flow rate in a discrete marking of an LFSPN equals $r$, the fact that refers to a particular condition from the fluid bisimulation definition. Thus, $\wr_{r}$ can be seen as a supplement to the PML and $HML_{MB}$ formula $\nabla_{a}$, where $a\in Act$, since $\nabla_{a}$ is used to check whether the transitions labeled with the action $a$ cannot be fired in a state (discrete marking), the fact violating the bisimulation transfer property.

Definition 8.4

Let $\top$ denote the truth and $a\in Act,\ r\in{\mathbb{R}},\ \lambda\in{\mathbb{R}}_{>0}$. A formula of $HML_{flb}$ is defined as follows:

[TABLE]

We define $\langle a\rangle\Phi=\exists\lambda\ \langle a\rangle_{\lambda}\Phi$ and $\Phi\vee\Psi=\neg(\neg\Phi\wedge\neg\Psi)$.

${\bf HML}_{flb}$ denotes the set of all formulas of the logic $HML_{flb}$.

Definition 8.5

Let $N$ be a LFSPN and $M\in DRS(N)$. The satisfaction relation $\models_{flb}\subseteq DRS(N)\times{\bf HML}_{flb}$ is defined as follows:

$M\models_{flb}\top$* — always;* 2. 2.

$M\models_{flb}\neg\Phi$, if $M\not\models_{N}\Phi$; 3. 3.

$M\models_{flb}\Phi\wedge\Psi$, if $M\models_{N}\Phi$ and $M\models_{N}\Psi$; 4. 4.

$M\models_{flb}\nabla_{a}$, if it does not hold that $M\stackrel{{\scriptstyle a}}{{\rightarrow}}DRS(N)$; 5. 5.

$M\models_{flb}\wr_{r}$, if $RP(M)=r$; 6. 6.

$M\models_{flb}\langle a\rangle_{\lambda}\Phi$, if $\exists{\cal H}\subseteq DRS(N)\ M\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\mu}{\cal H},\ \mu\geq\lambda$ and $\forall\widetilde{M}\in{\cal H}\ \widetilde{M}\models_{flb}\Phi$.

Note that $\langle a\rangle_{\mu}\Phi$ implies $\langle a\rangle_{\lambda}\Phi$, if $\mu\geq\lambda$.

Definition 8.6

Let $N$ be an LFSPN. Then we write $N\models_{flb}\Phi$, if $M_{N}\models_{flb}\Phi$. LFSPNs $N$ and $N^{\prime}$ are logically equivalent in $HML_{flb}$, denoted by $N=_{HML_{flb}}N^{\prime}$, if $\forall\Phi\in{\bf HML}_{flb}\ N\models_{flb}\Phi\ \Leftrightarrow\ N^{\prime}\models_{flb}\Phi$.

Let $N$ be an LFSPN and $M\in DRS(N),\ a\in Act$. The set of discrete markings reached from $M$ by execution of action $a$, called the image set, is defined as $Image(M,a)=\{\widetilde{M}\mid M\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M},\ L_{N}(t)=a\}$. An LFSPN $N$ is an image-finite one, if $\forall M\in DRS(N)\ \forall a\in Act\ |Image(M,a)|<\infty$.

Theorem 8.2

For image-finite LFSPNs $N$ and $N^{\prime}$

[TABLE]

Proof. Our reasoning is based on the proofs of Theorem 6.4 from [60] about characterization of probabilistic bisimulation equivalence for probabilistic transition systems and Theorem 1 from [37] about characterization of strong equivalence for PEPA. The differences are the LFSPNs context, and what we also respect the fluid flow rates in the discrete markings with the satisfaction check for the formulas $\wr_{r},\ r\in{\mathbb{R}}$, as presented below.

($\Leftarrow$) Let us define the equivalence relation ${\cal R}=\{(M_{1},M_{2})\in(DRS(N)\cup DRS(N^{\prime}))^{2}\mid\forall\Phi\in{\bf HML}_{flb}\\ M_{1}\models_{flb}\Phi\ \Leftrightarrow\ M_{2}\models_{flb}\Phi\}$. We have $(M_{N},M_{N^{\prime}})\in{\cal R}$. Let us prove that ${\cal R}$ is a fluid bisimulation.

Assume that $M_{N}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda}{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$. Let $M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda_{1}^{\prime}}M_{1}^{\prime},\ldots,M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda_{i}^{\prime}}M_{i}^{\prime},M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda_{i+1}^{\prime}}M_{i+1}^{\prime},\ldots,M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda_{n}^{\prime}}M_{n}^{\prime}$ be the changes of the discrete marking $M_{N^{\prime}}$ as a result of executing the action $a$. Since the LFSPN $N^{\prime}$ is image-finite one, the number of such changes is finite. The discrete marking changes are ordered so that $M_{1}^{\prime},\ldots,M_{i}^{\prime}\in{\cal H}$ and $M_{i+1}^{\prime},\ldots,M_{n}^{\prime}\not\in{\cal H}$.

Then $\exists\Phi_{i+1},\ldots,\Phi_{n}\in{\bf HML}_{flb}$ such that $\forall j\ (i+1\leq j\leq n)\ \forall M\in{\cal H}\ M\models_{flb}\Phi_{j}$, but $M_{j}^{\prime}\not\models_{flb}\Phi_{j}$. We have $M_{N}\models_{flb}\langle a\rangle_{\lambda}(\wedge_{j=i+1}^{n}\Phi_{j})$ and $M_{N^{\prime}}\models_{flb}\langle a\rangle_{\lambda^{\prime}}(\wedge_{j=i+1}^{n}\Phi_{j})$, where $\lambda^{\prime}=\sum_{j=1}^{i}\lambda_{j}^{\prime}$.

Assume that $\lambda>\lambda^{\prime}$. Then $M_{N^{\prime}}\not\models_{flb}\langle a\rangle_{\lambda}(\wedge_{j=i+1}^{n}\Phi_{j})$, which contradicts to $(M_{N},M_{N^{\prime}})\in{\cal R}$. Hence, $\lambda\leq\lambda^{\prime}$. Consequently, $M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\lambda^{\prime}}{\cal H}$, where $\lambda\leq\lambda^{\prime}$. By symmetry of ${\cal R}$, we have $\lambda\geq\lambda^{\prime}$. Thus, $\lambda=\lambda^{\prime}$, and ${\cal R}$ is a fluid bisimulation.

($\Rightarrow$) Let for LFSPNs $N$ and $N^{\prime}$ we have $N\underline{\leftrightarrow}_{fl}N^{\prime}$. Then $\exists{\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$ and $(M_{N},M_{N^{\prime}})\in{\cal R}$. It is sufficient to consider only the cases $\nabla_{a},\wr_{r}$ and $\langle a\rangle_{\lambda}\Phi$, since the remaining cases are trivial.

The case $\nabla_{a}$.

Assume that $M_{N}\models_{flb}\nabla_{a}$. Then it does not hold that $M_{N}\stackrel{{\scriptstyle a}}{{\rightarrow}}DRS(N)$. Hence, there exist no $t$ and $\widetilde{M}$ such that $M_{N}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M}$ and $L_{N}(t)=a$. Since summing by the empty index set produces zero, the transitions from each discrete marking always lead to the discrete markings of the discrete reachability set to which that discrete marking belongs and $(M_{N},M_{N^{\prime}})\in{\cal R}$, we get $0=\sum_{\{t\mid\exists\widetilde{M}\in DRS(N)\ M_{N}\stackrel{{\scriptstyle t}}{{\rightarrow}}\widetilde{M},\ L_{N}(t)=a\}}\Omega_{N}(t,M_{N})=\\ RM_{a}(M_{N},DRS(N))=RM_{a}(M_{N},DRS(N)\cup DRS(N^{\prime}))=\sum_{{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM_{a}(M_{N},{\cal H})=\\ \sum_{{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM_{a}(M_{N^{\prime}},{\cal H})=RM_{a}(M_{N^{\prime}},DRS(N)\cup DRS(N^{\prime}))=RM_{a}(M_{N^{\prime}},DRS(N^{\prime}))=\\ \sum_{\{t^{\prime}\mid\exists\widetilde{M}^{\prime}\in DRS(N^{\prime})\ M_{N^{\prime}}\stackrel{{\scriptstyle t^{\prime}}}{{\rightarrow}}\widetilde{M}^{\prime},\ L_{N^{\prime}}(t^{\prime})=a\}}\Omega_{N^{\prime}}(t^{\prime},M_{N^{\prime}})$. Hence, there exist no $t^{\prime}$ and $\widetilde{M}^{\prime}$ such that $M_{N^{\prime}}\stackrel{{\scriptstyle t^{\prime}}}{{\rightarrow}}\widetilde{M}^{\prime}$ and $L_{N^{\prime}}(t^{\prime})=a$. Thus, it does not hold that $M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}DRS(N^{\prime})$ and we have $M_{N^{\prime}}\models_{flb}\nabla_{a}$.

The case $\wr_{r}$.

Assume that $M_{N}\models_{flb}\wr_{r}$. Then, respecting that $(M_{N},M_{N^{\prime}})\in{\cal R}$, we get $r=RP(M_{N})=RP(M_{N^{\prime}})$, hence, $M_{N^{\prime}}\models_{flb}\wr_{r}$.

The case $\langle a\rangle_{\lambda}\Phi$.

Assume that $M_{N}\models_{flb}\langle a\rangle_{\lambda}\Phi$. Then $\exists{\cal H}\subseteq DRS(N)$ such that $M_{N}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\mu}{\cal H},\ \mu\geq\lambda$ and $\forall M\in{\cal H}\ M\models_{flb}\Phi$. Let us define $\widetilde{\cal H}=\bigcup\{\overline{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}\mid\overline{\cal H}\cap{\cal H}\neq\emptyset\}$. Then $\forall\widetilde{M}\in\widetilde{\cal H}\ \exists M\in{\cal H}\ (M,\widetilde{M})\in{\cal R}$. Since $\forall M\in{\cal H}\ M\models_{flb}\Phi$, we have $\forall\widetilde{M}\in\widetilde{\cal H}\ \widetilde{M}\models_{flb}\Phi$ by the induction hypothesis.

Since ${\cal H}\subseteq\widetilde{\cal H}$, we get $M_{N}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\tilde{\mu}}\widetilde{\cal H},\ \tilde{\mu}\geq\mu$. Since $\widetilde{\cal H}$ is the union of the equivalence classes with respect to ${\cal R}$, we have $(M_{N},M_{N^{\prime}})\in{\cal R}$ implies $M_{N^{\prime}}\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\tilde{\mu}}\widetilde{\cal H}$. Since $\tilde{\mu}\geq\mu\geq\lambda$, we get $M_{N^{\prime}}\models_{flb}\langle a\rangle_{\lambda}\Phi$. Therefore, $N^{\prime}$ satisfies all the formulas which $N$ does. By symmetry of ${\cal R},\ N$ satisfies all the formulas which $N^{\prime}$ does. Thus, the sets of satisfiable formulas for $N$ and $N^{\prime}$ coincide. $\sqcap\!\!\!\!\sqcup$

Thus, in the bisimulation semantics, we obtained a logical characterization of the fluid behavioural equivalence or, symmetrically, an operational characterization of the fluid modal logic equivalence.

Example 8.2

Consider the LFSPNs $N$ and $N^{\prime}$ from Figure 1, for which it holds $N\underline{\leftrightarrow}\!\!\!\!/\ _{fl}N^{\prime}$, hence, $N\neq_{HML_{flb}}N^{\prime}$. Indeed, for $\Phi=\langle a\rangle_{2}\langle b\rangle_{1}\top$ we have $N\models_{flb}\Phi$, but $N^{\prime}\not\models_{flb}\Phi$, since only in the LFSPN $N^{\prime}$ action $a$ can occur so that action $b$ cannot occur afterwards.

Let us now take the LFSPNs $N$ and $N^{\prime}$ from Figure 7, for which it holds $N\underline{\leftrightarrow}_{fl}N^{\prime}$, hence, $N=_{HML_{flb}}N^{\prime}$. In particular, for $\Psi=\wr_{1}\wedge\langle a\rangle_{2}(\wr_{-2}\wedge\langle b\rangle_{2}\top)$ we have $N\models_{flb}\Psi$ and $N^{\prime}\models_{flb}\Psi$.

Table 2 demonstrates how the modalities and interpretation functions of the logics $HML_{flt}$ and $HML_{flb}$ respect the following behavioural aspects of LFSPNs: semantics type (linear or branching time), functional activity (consisting in the action occurrences), stochastic timing (specified by the transition rates) and fluid flow (defined by the fluid rates). In case of the composite constructions, the variables describing particular aspects of behaviour are presented nearby in parentheses.

9 Preservation of the quantitative behaviour

It is clear that the proposed fluid bisimulation equivalence of LFSPNs preserves their qualitative (functional) behaviour which is based on the actions assigned to the fired transitions. Let us examine if fluid bisimulation equivalence also preserves the quantitative (performance) behaviour of LFSPNs, taken for the steady states of their underlying CTMCs and associated SFMs. The quantitative behaviour takes into account the values of the rates and probabilities, as well as those of the related probability mass, distribution, density and mass at lower boundary functions. Then we shall define the quotients of the mentioned probability functions by fluid bisimulation equivalence with a goal to describe the quotient (by $\underline{\leftrightarrow}_{fl}$) associated SFMs.

The following proposition demonstrates that for two LFSPNs related by $\underline{\leftrightarrow}_{fl}$ their aggregate steady-state probabilities coincide for each equivalence class of discrete markings.

Proposition 9.1

Let $N,N^{\prime}$ be LFSPNs with ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$ and $\varphi=(\varphi_{1},\ldots,\varphi_{n}),\ n=|DRS(N)|$, be the steady-state PMF for $CTMC(N)$ and $\varphi^{\prime}=(\varphi_{1}^{\prime},\ldots,\varphi_{m}^{\prime}),\ m=|DRS(N^{\prime})|$, be the steady-state PMF for $CTMC(N^{\prime})$. Then for all ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$ we have

[TABLE]

Proof. The steady-state PMF $\varphi=(\varphi_{1},\ldots,\varphi_{n})$ for $CTMC(N)$ is a solution of the linear equation system

[TABLE]

Then for all $i\ (1\leq i\leq n)$ we have

[TABLE]

By definition of ${\cal Q}_{ij}\ (1\leq i,j\leq n)$ we have

[TABLE]

Let ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$. We sum the left and right sides of the first equation from the system above for all $i$ such that $M_{i}\in{\cal H}\cap DRS(N)$. The resulting equation is

[TABLE]

Let us denote the aggregate steady-state PMF for $CTMC(N)$ by $\varphi_{{\cal H}\cap DRS(N)}=\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\varphi_{i}$. Then, by Remark 2 from Section 6, for the left-hand side of the equation above, we get

$\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\sum_{j=1}^{n}RM(M_{j},M_{i})\varphi_{j}=\sum_{j=1}^{n}\varphi_{j}\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}RM(M_{j},M_{i})=\\ \sum_{j=1}^{n}RM(M_{j},{\cal H})\varphi_{j}=\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}RM(M_{j},{\cal H})\varphi_{j}=\\ \sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}RM(\widetilde{\cal H},{\cal H})\varphi_{j}=\\ \sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(\widetilde{\cal H},{\cal H})\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}\varphi_{j}\!=\!\!\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(\widetilde{\cal H},{\cal H})\varphi_{\widetilde{\cal H}\cap DRS(N)}$.

For the left-hand side of the second equation from the system above, we have

$\sum_{j=1}^{n}\varphi_{j}=\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}\varphi_{j}=\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\varphi_{{\cal H}\cap DRS(N)}$.

Thus, the aggregate linear equation system for $CTMC(N)$ is

[TABLE]

Let us denote the aggregate steady-state PMF for $CTMC(N^{\prime})$ by $\varphi_{{\cal H}\cap DRS(N^{\prime})}^{\prime}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}$. Then, in a similar way, the aggregate linear equation system for $CTMC(N^{\prime})$ is

[TABLE]

Let $(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}=\{{\cal H}_{1},\ldots,{\cal H}_{l}\}$. Then the aggregate steady-state PMFs $\varphi_{{\cal H}_{k}\cap DRS(N)}$ and $\varphi_{{\cal H}_{k}\cap DRS(N^{\prime})}^{\prime}\ (1\leq k\leq l)$ satisfy the same aggregate system of $l+1$ linear equations with $l$ independent equations and $l$ unknowns. The aggregate linear equation system has a unique solution when a single aggregate steady-state PMF exists, which is the case here. Hence, $\varphi_{{\cal H}_{k}\cap DRS(N)}=\varphi_{{\cal H}_{k}\cap DRS(N^{\prime})}^{\prime}\ (1\leq k\leq l)$. $\sqcap\!\!\!\!\sqcup$

Let $N$ be an LFSPN and $\varphi$ be the steady-state PMF for $CTMC(N)$. Let $\varphi_{\cal K},\ {\cal K}\in DRS(N)/_{{\cal R}_{fl}}(N)$, be the elements of the steady-state PMF for $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$, denoted by $\varphi_{\underline{\leftrightarrow}_{fl}}$. By (the proof of) Proposition 9.1, for all ${\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$ we have

[TABLE]

Let ${\bf V}$ be the collector matrix for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$. One can see that

[TABLE]

We have \left\{\begin{array}[]{l}\varphi{\bf Q}={\bf 0}\\ \varphi{\bf 1}^{T}=1\end{array}\right.. After right-multiplying both sides of the first equation by ${\bf V}$ and since ${\bf V}{\bf 1}^{T}={\bf 1}^{T}$, we get \left\{\begin{array}[]{l}\varphi{\bf Q}{\bf V}={\bf 0}\\ \varphi{\bf V}{\bf 1}^{T}=1\end{array}\right.. Since ${\bf Q}{\bf V}={\bf V}{\bf Q}_{\underline{\leftrightarrow}_{fl}}$, we obtain \left\{\begin{array}[]{l}\varphi{\bf V}{\bf Q}_{\underline{\leftrightarrow}_{fl}}={\bf 0}\\ \varphi{\bf V}{\bf 1}^{T}=1\end{array}\right.. Since $\varphi{\bf V}=\varphi_{\underline{\leftrightarrow}_{fl}}$, we conclude that $\varphi_{\underline{\leftrightarrow}_{fl}}$ is a solution of the linear equation system

[TABLE]

Thus, the treatment of $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ instead of $CTMC(N)$ simplifies the analytical solution, since we have less states, but constructing the TRM ${\bf Q}_{\underline{\leftrightarrow}_{fl}}$ for $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ also requires some efforts, including determining ${\cal R}_{fl}(N)$ and calculating the rates to move from one equivalence class to another. The behaviour of $CTMC_{\underline{\leftrightarrow}_{fl}}(N)$ stabilizes quicker than that of $CTMC(N)$ (if each of them has a single steady state), since ${\bf Q}_{\underline{\leftrightarrow}_{fl}}$ is denser matrix than ${\bf Q}$ (the TRM for $CTMC(N)$) due to the fact that the former matrix is smaller and the transitions between the equivalence classes “include” all the transitions between the discrete markings belonging to these equivalence classes.

The following proposition demonstrates that for two LFSPNs related by $\underline{\leftrightarrow}_{fl}$ their aggregate steady-state fluid PDFs coincide for each equivalence class of discrete markings.

Proposition 9.2

Let $N,N^{\prime}$ be LFSPNs with ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$ and $F(x)=(F_{1}(x),\ldots,F_{n}(x)),\ n=|DRS(N)|$, be the steady-state fluid PDF for the SFM of $N$ and $F^{\prime}(x)=(F_{1}^{\prime}(x),\ldots,F_{m}^{\prime}(x)),\ m=|DRS(N^{\prime})|$, be the steady-state fluid PDF for the SFM of $N^{\prime}$. Then for all ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$ we have

[TABLE]

Proof. The ordinary differential equation characterizing the steady-state PDF for the SFM of $N$ is

[TABLE]

The upper boundary constraint is $F(\infty)=\varphi$, where $\varphi$ is the steady-state PMF for $CTMC(N)$.

Then for all $i\ (1\leq i\leq n)$ we have

[TABLE]

The upper boundary constraints are $\forall i\ (1\leq i\leq n)\ F_{i}(\infty)=\varphi_{i}$, where $\varphi=(\varphi_{1},\ldots,\varphi_{n})$ is the steady-state PMF for $CTMC(N)$.

By definition of ${\cal R}_{ij}$ and ${\cal Q}_{ij}\ (1\leq i,j\leq n)$ we have

[TABLE]

Let ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$. We sum the left and right sides of the equation above for all $i$ such that $M_{i}\in{\cal H}\cap DRS(N)$. The resulting equation is

[TABLE]

Let us denote the aggregate fluid flow PDF for the SFM of $N$ by $F_{{\cal H}\cap DRS(N)}(x)=\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}F_{i}(x)$. Then, by Remark 3 from Section 6, for the left-hand side of the equation above, we get

$\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}RP(M_{i})\frac{dF_{i}(x)}{dx}=\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}RP({\cal H})\frac{dF_{i}(x)}{dx}=RP({\cal H})\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\frac{dF_{i}(x)}{dx}=\\ RP({\cal H})\frac{d}{dx}\left(\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}F_{i}(x)\right)=RP({\cal H})\frac{dF_{{\cal H}\cap DRS(N)}(x)}{dx}$.

Analogously, for the right-hand side of the equation above, we get

$\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\sum_{j=1}^{n}RM(M_{j},M_{i})F_{j}(x)=\sum_{j=1}^{n}F_{j}(x)\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}RM(M_{j},M_{i})=\\ \sum_{j=1}^{n}RM(M_{j},{\cal H})F_{j}(x)=\sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}RM(M_{j},{\cal H})F_{j}(x)=\\ \sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}RM(\widetilde{\cal H},{\cal H})F_{j}(x)=\\ \sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(\widetilde{\cal H},{\cal H})\sum_{\{j\mid M_{j}\in\widetilde{\cal H}\cap DRS(N)\}}F_{j}(x)=\\ \sum_{\widetilde{\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}}RM(\widetilde{\cal H},{\cal H})F_{\widetilde{\cal H}\cap DRS(N)}(x)$.

By combining both the resulting sides of the differential equation, we get the aggregate differential equation system for the SFM of $N$:

[TABLE]

Let us denote the aggregate fluid flow PDF for the SFM of $N^{\prime}$ by $F_{{\cal H}\cap DRS(N^{\prime})}^{\prime}(x)=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}F_{j}^{\prime}(x)$. Then, in a similar way, we get the aggregate differential equation system for the SFM of $N^{\prime}$:

[TABLE]

By Proposition 9.1, the upper boundary constraints associated with the aggregate differential equation systems for the SFMs of $N$ and $N^{\prime}$ coincide: $F_{{\cal H}\cap DRS(N)}(\infty)=\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}F_{i}(\infty)=\\ \sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\varphi_{i}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}\varphi_{i}^{\prime}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}F_{j}^{\prime}(\infty)=F_{{\cal H}\cap DRS(N^{\prime})}^{\prime}(\infty)$.

Let $(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}=\{{\cal H}_{1},\ldots,{\cal H}_{l}\}$. By analogy with the above results for ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$, we can demonstrate that for each ${\cal H}_{k}\ (1\leq k\leq l)$ the aggregate differential equation systems for the SFMs of $N$ and $N^{\prime}$ and the associated upper boundary constraints coincide.

For each ${\cal H}_{k}\ (1\leq k\leq l)$, the lower boundary constraints are $\exists M_{i}\in{\cal H}_{k}\cap DRS(N)\ RP(M_{i})>0\ \Rightarrow\ F_{i}(0)=0$ and $\exists M_{j}^{\prime}\in{\cal H}_{k}\cap DRS(N^{\prime})\ RP(M_{j}^{\prime})>0\ \Rightarrow\ F_{j}^{\prime}(0)=0$. Since $\forall M_{i}\in{\cal H}_{k}\cap DRS(N)\ \forall M_{j}^{\prime}\in{\cal H}_{k}\cap DRS(N^{\prime})\ RP(M_{i})=RP({\cal H}_{k}\cap DRS(N))=RP({\cal H}_{k})=RP({\cal H}_{k}\cap DRS(N^{\prime}))=RP(M_{j}^{\prime})$, we have $F_{{\cal H}_{k}\cap DRS(N)}(0)=0\ \Leftarrow\ RP({\cal H}_{k})>0\ \Rightarrow\ F_{{\cal H}_{k}\cap DRS(N^{\prime})}^{\prime}(0)=0\ (1\leq k\leq l)$.

Then the aggregate fluid flow PDFs $F_{{\cal H}_{k}\cap DRS(N)}(x)$ and $F_{{\cal H}_{k}\cap DRS(N^{\prime})}^{\prime}(x)\ (1\leq k\leq l)$ satisfy the same aggregate system of $l$ differential equations with $l$ unknowns and the same upper and lower boundary constraints. The spectral decomposition method, described in Section 4, provides such an aggregate differential equation system with a unique solution. Hence, $F_{{\cal H}_{k}\cap DRS(N)}(x)=F_{{\cal H}_{k}\cap DRS(N^{\prime})}^{\prime}(x)\ (1\leq k\leq l)$. $\sqcap\!\!\!\!\sqcup$

Let $N$ be an LFSPN and $F(x)$ be the steady-state fluid PDF for the SFM of $N$. Let $F_{\cal K}(x),\ {\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$, be the elements of the steady-state fluid PDF for the quotient (by $\underline{\leftrightarrow}_{fl}$) SFM of $N$, denoted by $F_{\underline{\leftrightarrow}_{fl}}(x)$. By (the proof of) Proposition 9.2, for all ${\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$ we have

[TABLE]

Let ${\bf V}$ be the collector matrix for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$. One can see that

[TABLE]

We have $\frac{dF(x)}{dx}{\bf R}=F(x){\bf Q},\ x>0$. After right-multiplying both sides of the above equation by ${\bf V}$, we get $\frac{dF(x)}{dx}{\bf R}{\bf V}=F(x){\bf Q}{\bf V},\ x>0$. Since ${\bf R}{\bf V}={\bf V}{\bf R}_{\underline{\leftrightarrow}_{fl}}$ and ${\bf Q}{\bf V}={\bf V}{\bf Q}_{\underline{\leftrightarrow}_{fl}}$, we obtain $\frac{dF(x)}{dx}{\bf V}{\bf R}_{\underline{\leftrightarrow}_{fl}}=F(x){\bf V}{\bf Q}_{\underline{\leftrightarrow}_{fl}},\\ x>0$. By linearity of differentiation operator, we have $\frac{d}{dx}(F(x){\bf V}){\bf R}_{\underline{\leftrightarrow}_{fl}}=F(x){\bf V}{\bf Q}_{\underline{\leftrightarrow}_{fl}},\ x>0$. Since $F(x){\bf V}=F_{\underline{\leftrightarrow}_{fl}}(x)$, we conclude that $F_{\underline{\leftrightarrow}_{fl}}(x)$ is a solution of the system of ordinary differential equations

[TABLE]

Thus, the treatment of the quotient (by $\underline{\leftrightarrow}_{fl}$) SFM of $N$ instead of SFM of $N$ simplifies the analytical solution.

The following proposition demonstrates that for two LFSPNs related by $\underline{\leftrightarrow}_{fl}$ their aggregate steady-state fluid probability density functions coincide for each equivalence class of discrete markings.

Proposition 9.3

Let $N,N^{\prime}$ be LFSPNs with ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$ and $f(x)=(f_{1}(x),\ldots,f_{n}(x)),\ n=|DRS(N)|$, be the steady-state fluid probability density function for the SFM of $N$ and $f^{\prime}(x)=(f_{1}^{\prime}(x),\ldots,f_{m}^{\prime}(x)),\ m=|DRS(N^{\prime})|$, be the steady-state fluid probability density function for the SFM of $N^{\prime}$. Then for all ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$ we have

[TABLE]

Proof. Remember that $f_{i}(x)=\frac{dF_{i}(x)}{dx}\ (1\leq i\leq n)$ and $f_{j}^{\prime}(x)=\frac{dF_{j}^{\prime}(x)}{dx}\ (1\leq j\leq m)$. Let ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$. By Proposition 9.2, we have

[TABLE]

By differentiating both sides of this equation by $x$ and applying the property for differentiating a sum, we get

[TABLE]

$\sqcap\!\!\!\!\sqcup$

Let $N$ be an LFSPN and $f(x)$ be the steady-state fluid probability density function for the SFM of $N$. Let $f_{\cal K}(x),\ {\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$, be the elements of the steady-state fluid probability density function for the quotient (by $\underline{\leftrightarrow}_{fl}$) SFM of $N$, denoted by $f_{\underline{\leftrightarrow}_{fl}}(x)$. By (the proof of) Proposition 9.3, for all ${\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$ we have

[TABLE]

Let ${\bf V}$ be the collector matrix for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$. One can see that

[TABLE]

We have $\frac{df(x)}{dx}{\bf R}=f(x){\bf Q},\ x>0$. Like it has been done after Proposition 9.2, we can prove that $f_{\underline{\leftrightarrow}_{fl}}(x)$ is a solution of the system of ordinary differential equations

[TABLE]

Alternatively, we can use the fact $f(x)=\frac{dF(x)}{dx}$. Since $f(x){\bf V}=f_{\underline{\leftrightarrow}_{fl}}(x),\ x>0$, and $F(x){\bf V}=F_{\underline{\leftrightarrow}_{fl}}(x),\\ x>0$, by linearity of differentiation operator, we have $f_{\underline{\leftrightarrow}_{fl}}(x)=f(x){\bf V}=\frac{dF(x)}{dx}{\bf V}=\frac{d}{dx}(F(x){\bf V})=\frac{dF_{\underline{\leftrightarrow}_{fl}}(x)}{dx}$.

We also have $\frac{dF_{\underline{\leftrightarrow}_{fl}}(x)}{dx}{\bf R}_{\underline{\leftrightarrow}_{fl}}=F_{\underline{\leftrightarrow}_{fl}}(x){\bf Q}_{\underline{\leftrightarrow}_{fl}},\ x>0$. Since $f_{\underline{\leftrightarrow}_{fl}}(x)=\frac{dF_{\underline{\leftrightarrow}_{fl}}(x)}{dx}$, by differentiating both sides of the previous equation, we get $\frac{d}{dx}\left(f_{\underline{\leftrightarrow}_{fl}}(x){\bf R}_{\underline{\leftrightarrow}_{fl}}\right)=\frac{d}{dx}\left(F_{\underline{\leftrightarrow}_{fl}}(x){\bf Q}_{\underline{\leftrightarrow}_{fl}}\right),\ x>0$. By linearity of differentiation operator and since $f_{\underline{\leftrightarrow}_{fl}}(x)=\frac{dF_{\underline{\leftrightarrow}_{fl}}(x)}{dx}$, we conclude that $f_{\underline{\leftrightarrow}_{fl}}(x)$ is a solution of the system of ordinary differential equations

[TABLE]

The following proposition demonstrates that for two LFSPNs related by $\underline{\leftrightarrow}_{fl}$ their aggregate steady-state buffer empty probabilities coincide for each equivalence class of discrete markings.

Proposition 9.4

Let $N,N^{\prime}$ be LFSPNs with ${\cal R}:N\underline{\leftrightarrow}_{fl}N^{\prime}$ and $\ell=(\ell_{1},\ldots,\ell_{n}),\ n=|DRS(N)|$, be the steady-state buffer empty probability for the SFM of $N$ and $\ell^{\prime}(x)=(\ell_{1}^{\prime},\ldots,\ell_{m}^{\prime}),\ m=|DRS(N^{\prime})|$, be the steady-state buffer empty probability for the SFM of $N^{\prime}$. Then for all ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$ we have

[TABLE]

Proof. Remember that by the total probability law for the stationary behaviour for the SFM of $N$, we have

[TABLE]

Then for all $i\ (1\leq i\leq n)$ we have

[TABLE]

Let ${\cal H}\in(DRS(N)\cup DRS(N^{\prime}))/_{\cal R}$. We sum the left and right sides of the equation above for all $i$ such that $M_{i}\in{\cal H}\cap DRS(N)$. The resulting equation is

[TABLE]

Consider the right-hand side of the equation above. We apply to it the property for integrating a sum, then Proposition 9.1 and Proposition 9.3, finally, the total probability law for the stationary behaviour for the SFM of $N$. Then we get $\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\ell_{i}=\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\varphi_{i}-\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\int_{0+}^{\infty}f_{i}(x)dx=\\ \sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}\varphi_{i}-\int_{0+}^{\infty}\sum_{\{i\mid M_{i}\in{\cal H}\cap DRS(N)\}}f_{i}(x)dx=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}\varphi_{i}^{\prime}-\\ \int_{0+}^{\infty}\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}f_{i}^{\prime}(x)dx=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}\varphi_{i}^{\prime}-\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}\int_{0+}^{\infty}f_{i}^{\prime}(x)dx=\\ \sum_{\{j\mid M_{j}^{\prime}\in{\cal H}\cap DRS(N^{\prime})\}}\ell_{j}^{\prime}$. $\sqcap\!\!\!\!\sqcup$

Let $N$ be an LFSPN and $\ell$ be the steady-state buffer empty probability for the SFM of $N$. Let $\ell_{\cal K},\ {\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$, be the elements of the steady-state buffer empty probability for the quotient (by $\underline{\leftrightarrow}_{fl}$) SFM of $N$, denoted by $\ell_{\underline{\leftrightarrow}_{fl}}$. By (the proof of) Proposition 9.4, for all ${\cal K}\in DRS(N)/_{{\cal R}_{fl}(N)}$ we have

[TABLE]

Let ${\bf V}$ be the collector matrix for the largest fluid autobisimulation ${\cal R}_{fl}(N)$ on $N$. One can see that

[TABLE]

We have $\ell=\varphi-\int_{0+}^{\infty}f(x)dx$. After right-multiplying both sides of the equation by ${\bf V}$, we get $\ell{\bf V}=\varphi{\bf V}-\left(\int_{0+}^{\infty}f(x)dx\right){\bf V}$. Since $\ell{\bf V}=\ell_{\underline{\leftrightarrow}_{fl}}$ and $\varphi{\bf V}=\varphi_{\underline{\leftrightarrow}_{fl}}$, by linearity of integration operator, we obtain $\ell_{\underline{\leftrightarrow}_{fl}}=\varphi_{\underline{\leftrightarrow}_{fl}}-\int_{0+}^{\infty}f(x){\bf V}dx$. Since $f(x){\bf V}=f_{\underline{\leftrightarrow}_{fl}}(x),\ x>0$, we conclude that $\ell_{\underline{\leftrightarrow}_{fl}}$ is a solution of the linear equation system

[TABLE]

Thus, the proposed quotients of the probability functions describe the behaviour of the quotient (by $\underline{\leftrightarrow}_{fl}$) associated SFMs of LFSPNs.

Example 9.1

Consider the LFSPNs $N$ and $N^{\prime}$ from Figure 7, for which it holds $N\underline{\leftrightarrow}_{fl}N^{\prime}$.

We have $DRS^{-}(N)=\{M_{2}\},\ DRS^{0}(N)=\emptyset$ and $DRS^{+}(N)=\{M_{1}\}$.

The steady-state PMF for $CTMC(N)$ is

[TABLE]

Then the stability condition for the SFM of $N$ is fulfilled: $FluidFlow(q)=\sum_{i=1}^{2}\varphi_{i}RP(M_{i})=\frac{1}{2}\cdot 1+\frac{1}{2}(-2)=-\frac{1}{2}<0$.

For each eigenvalue $\gamma$ we must have |\gamma{\bf R}-{\bf Q}|=\left|\begin{array}[]{cc}\gamma+2&-2\\ -2&-2\gamma+2\end{array}\right|=-2\gamma(1+\gamma)=0; hence, $\gamma_{1}=0$ and $\gamma_{2}=-1$.

The corresponding eigenvectors are the solutions of

[TABLE]

Then the (normalized) eigenvectors are $v_{1}=\left(\frac{1}{2},\frac{1}{2}\right)$ and $v_{2}=\left(\frac{2}{3},\frac{1}{3}\right)$.

Since $\varphi=F(\infty)=a_{1}v_{1}$, we have $F(x)=\varphi+a_{2}e^{\gamma_{2}x}v_{2}$ and $a_{1}=1$. Since $\forall M_{l}\in DRS^{+}(N)\\ F_{l}(0)=\varphi_{l}+a_{2}v_{2l}=0$ and $DRS^{+}(N)=\{M_{1}\}$, we have $\varphi_{1}+a_{2}v_{21}=\frac{1}{2}+a_{2}\frac{2}{3}=0$; hence, $a_{2}=-\frac{3}{4}$.

Then the steady-state fluid PDF for the SFM of $N$ is

[TABLE]

The steady-state fluid probability density function for the SFM of $N$ is

[TABLE]

The steady-state buffer empty probability for the SFM of $N$ is

[TABLE]

We have $DRS^{-}(N^{\prime})=\{M_{2}^{\prime},M_{3}^{\prime}\},\ DRS^{0}(N^{\prime})=\emptyset$ and $DRS^{+}(N^{\prime})=\{M_{1}^{\prime}\}$.

The steady-state PMF for $CTMC(N^{\prime})$ is

[TABLE]

Then the stability condition for the SFM of $N^{\prime}$ is fulfilled: $FluidFlow(q^{\prime})=\sum_{j=1}^{3}\varphi_{j}^{\prime}RP(M_{j}^{\prime})=\frac{1}{2}\cdot 1+\frac{1}{4}(-2)+\frac{1}{4}(-2)=-\frac{1}{2}<0$.

For each eigenvalue $\gamma^{\prime}$ we must have |\gamma^{\prime}{\bf R}^{\prime}-{\bf Q}^{\prime}|=\left|\begin{array}[]{ccc}\gamma^{\prime}+2&-1&-1\\ -2&-2\gamma^{\prime}+2&0\\ -2&0&-2\gamma^{\prime}+2\end{array}\right|=-2\gamma^{\prime}(1+\gamma^{\prime})(1-\gamma^{\prime})=0; hence, $\gamma_{1}^{\prime}=0,\ \gamma_{2}^{\prime}=-1$ and $\gamma_{3}^{\prime}=1$.

By the boundedness condition, the positive eigenvalue $\gamma_{3}^{\prime}$ and the corresponding eigenvector $v_{3}^{\prime}$ should be excluded from the solution.

The remaining corresponding eigenvectors are the solutions of

[TABLE]

Then the remaining (normalized) eigenvectors are $v_{1}^{\prime}=\left(\frac{1}{2},\frac{1}{4},\frac{1}{4}\right)$ and $v_{2}^{\prime}=\left(\frac{2}{3},\frac{1}{6},\frac{1}{6}\right)$.

Since $\varphi^{\prime}=F^{\prime}(\infty)=a_{1}^{\prime}v_{1}^{\prime}$, we have $F^{\prime}(x)=\varphi^{\prime}+a_{2}^{\prime}e^{\gamma_{2}^{\prime}x}v_{2}^{\prime}$ and $a_{1}^{\prime}=1$. Since $\forall M_{l}^{\prime}\in DRS^{+}(N^{\prime})\\ F_{l}^{\prime}(0)=\varphi_{l}^{\prime}+a_{2}^{\prime}v_{2l}^{\prime}=0$ and $DRS^{+}(N^{\prime})=\{M_{1}^{\prime}\}$, we have $\varphi_{1}^{\prime}+a_{2}^{\prime}v_{21}^{\prime}=\frac{1}{2}+a_{2}^{\prime}\frac{2}{3}=0$; hence, $a_{2}=-\frac{3}{4}$.

Then the steady-state fluid PDF for the SFM of $N^{\prime}$ is

[TABLE]

The steady-state fluid probability density function for the SFM of $N^{\prime}$ is

[TABLE]

The steady-state buffer empty probability for the SFM of $N^{\prime}$ is

[TABLE]

In Figure 11, the plots of the elements $F_{1},F_{2},F_{2}^{\prime}$ of the steady-state fluid PDFs $F=(F_{1},F_{2})$ and $F^{\prime}=(F_{1}^{\prime},F_{2}^{\prime},F_{3}^{\prime})$ for the SFMs of $N$ and $N^{\prime}$ as functions of $x$ are depicted. It is sufficient to consider the functions $F_{1}(x)=\frac{1}{2}-\frac{1}{2}e^{-x},\ F_{2}(x)=\frac{1}{2}-\frac{1}{4}e^{-x},\ F_{2}^{\prime}(x)=\frac{1}{4}-\frac{1}{8}e^{-x}$ only, since $F_{1}=F_{1}^{\prime}$ and $F_{2}^{\prime}=F_{3}^{\prime}$.

We have $(DRS(N)\cup DRS(N^{\prime}))/_{{\cal R}_{fl}(N,N^{\prime})}=\{{\cal H}_{1},{\cal H}_{2}\}$, where ${\cal H}_{1}=\{M_{1},M_{1}^{\prime}\}$ and ${\cal H}_{2}=\{M_{2},M_{2}^{\prime},M_{3}^{\prime}\}$.

First, consider the equivalence class ${\cal H}_{1}$.

• •

The aggregate steady-state probabilities for ${\cal H}_{1}$ coincide: $\varphi_{{\cal H}_{1}\cap DRS(N)}=\sum_{\{i\mid M_{i}\in{\cal H}_{1}\cap DRS(N)\}}\varphi_{i}=\varphi_{1}=\frac{1}{2}=\varphi_{1}^{\prime}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{1}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}=\varphi_{{\cal H}_{1}\cap DRS(N^{\prime})}^{\prime}$.

• •

The aggregate steady-state buffer empty probabilities for ${\cal H}_{1}$ coincide: $\ell_{{\cal H}_{1}\cap DRS(N)}=\\ \sum_{\{i\mid M_{i}\in{\cal H}_{1}\cap DRS(N)\}}\ell_{i}=\ell_{1}=0=\ell_{1}^{\prime}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{1}\cap DRS(N^{\prime})\}}\ell_{j}^{\prime}=\ell_{{\cal H}_{1}\cap DRS(N^{\prime})}^{\prime}$.

• •

The aggregate steady-state fluid PDFs for ${\cal H}_{1}$ coincide: $F_{{\cal H}_{1}\cap DRS(N)}(x)=\sum_{\{i\mid M_{i}\in{\cal H}_{1}\cap DRS(N)\}}F_{i}(x)=F_{1}(x)=\frac{1}{2}-\frac{1}{2}e^{-x}=F_{1}^{\prime}(x)=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{1}\cap DRS(N^{\prime})\}}F_{j}^{\prime}(x)=F_{{\cal H}_{1}\cap DRS(N^{\prime})}^{\prime}(x)$, where $x>0$.

• •

The aggregate steady-state fluid probability density functions for ${\cal H}_{1}$ coincide: $f_{{\cal H}_{1}\cap DRS(N)}(x)=\\ \sum_{\{i\mid M_{i}\in{\cal H}_{1}\cap DRS(N)\}}f_{i}(x)=f_{1}(x)=\frac{1}{2}e^{-x}=f_{1}^{\prime}(x)=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{1}\cap DRS(N^{\prime})\}}f_{j}^{\prime}(x)=f_{{\cal H}_{1}\cap DRS(N^{\prime})}^{\prime}(x)$, where $x>0$.

Second, consider the equivalence class ${\cal H}_{2}$.

• •

The aggregate steady-state probabilities for ${\cal H}_{2}$ coincide: $\varphi_{{\cal H}_{2}\cap DRS(N)}=\sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\varphi_{i}=\varphi_{2}=\\ \frac{1}{2}=\frac{1}{4}+\frac{1}{4}=\varphi_{2}^{\prime}+\varphi_{3}^{\prime}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}=\varphi_{{\cal H}_{2}\cap DRS(N^{\prime})}^{\prime}$.

• •

The aggregate steady-state buffer empty probabilities for ${\cal H}_{2}$ coincide: $\ell_{{\cal H}_{2}\cap DRS(N)}=\\ \sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\ell_{i}=\ell_{2}=\frac{1}{4}=\frac{1}{8}+\frac{1}{8}=\ell_{2}^{\prime}+\ell_{3}^{\prime}=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\ell_{j}^{\prime}=\ell_{{\cal H}_{2}\cap DRS(N^{\prime})}^{\prime}$.

• •

The aggregate steady-state fluid PDFs for ${\cal H}_{2}$ coincide: $F_{{\cal H}_{2}\cap DRS(N)}(x)=\sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}F_{i}(x)=\\ F_{2}(x)=\frac{1}{2}-\frac{1}{4}e^{-x}=\frac{1}{4}-\frac{1}{8}e^{-x}+\frac{1}{4}-\frac{1}{8}e^{-x}=F_{2}^{\prime}(x)+F_{3}^{\prime}(x)=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}F_{j}^{\prime}(x)=F_{{\cal H}_{2}\cap DRS(N^{\prime})}^{\prime}(x)$, where $x>0$.

• •

The aggregate steady-state fluid probability density functions for ${\cal H}_{2}$ coincide: $f_{{\cal H}_{2}\cap DRS(N)}(x)=\\ \sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}f_{i}(x)=f_{2}(x)=\frac{1}{4}e^{-x}=\frac{1}{8}e^{-x}+\frac{1}{8}e^{-x}=f_{2}^{\prime}(x)+f_{3}^{\prime}(x)=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}f_{j}^{\prime}(x)=f_{{\cal H}_{2}\cap DRS(N^{\prime})}^{\prime}(x)$, where $x>0$.

One can also see that $\varphi_{\underline{\leftrightarrow}_{fl}}=\varphi_{\underline{\leftrightarrow}_{fl}}^{\prime}=\varphi,\ \ell_{\underline{\leftrightarrow}_{fl}}=\ell_{\underline{\leftrightarrow}_{fl}}^{\prime}=\ell,\ F_{\underline{\leftrightarrow}_{fl}}(x)=F_{\underline{\leftrightarrow}_{fl}}^{\prime}(x)=F(x),\ x>0$, and $f_{\underline{\leftrightarrow}_{fl}}(x)=f_{\underline{\leftrightarrow}_{fl}}^{\prime}(x)=f(x),\ x>0$.

10 Preservation of the functionality and performance

In this section we demonstrate how fluid bisimulation equivalence preserves the functionality and performance of the equivalent LFSPNs.

Consider the LFSPNs $N$ and $N^{\prime}$ from Figure 7, for which it holds $N\underline{\leftrightarrow}_{fl}N^{\prime}$.

Many steady-state hybrid performance indices may be aggregated to make them consistent with fluid bisimulation, as well as with the quotienting of the discrete reachability graphs and underlying CTMCs, and with the induced lumping of the discrete markings into the equivalence classes. Thus, the aggregate (up to $\underline{\leftrightarrow}_{fl}$) steady-state performance measures of $N$ based on the probability functions $\varphi,\ell,F(x)$ and $f(x)$ should coincide with those of $N^{\prime}$ based on $\varphi^{\prime},\ell^{\prime},F^{\prime}(x)$ and $f^{\prime}(x)$, respectively. Let us check this for the equivalence class ${\cal H}_{2}$.

• •

The aggregate fraction (proportion) of time spent in the set of discrete markings ${\cal H}_{2}\cap DRS(N)$ is

$TimeFract({\cal H}_{2}\cap DRS(N))=\sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\varphi_{i}=\varphi_{2}=\frac{1}{2}$.

The aggregate fraction (proportion) of time spent in the set of discrete markings ${\cal H}_{2}\cap DRS(N^{\prime})$ is

$TimeFract({\cal H}_{2}\cap DRS(N^{\prime}))=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\varphi_{i}^{\prime}=\varphi_{2}^{\prime}+\varphi_{3}^{\prime}=\frac{1}{4}+\frac{1}{4}=\frac{1}{2}$.

• •

The aggregate firing frequency (throughput) of the transitions enabled in the discrete markings from

${\cal H}_{2}\cap DRS(N)$ is $FiringFreq_{{\cal H}_{2}\cap DRS(N)}=\sum_{t\in T_{N}}FiringFreq_{{\cal H}_{2}\cap DRS(N)}(t)=\\ \sum_{t\in T_{N}}\sum_{\{i\mid t\in Ena(M_{i}),\ M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\varphi_{i}\Omega_{N}(t,M_{i})=\varphi_{2}\Omega_{N}(t_{2},M_{2})+\varphi_{2}\Omega_{N}(t_{3},M_{2})=\frac{1}{2}\cdot 1+\frac{1}{2}\cdot 1=\frac{1}{2}+\frac{1}{2}=1$.

The aggregate firing frequency (throughput) of the transitions enabled in the discrete markings from

${\cal H}_{2}\cap DRS(N^{\prime})$ is $FiringFreq_{{\cal H}_{2}\cap DRS(N^{\prime})}=\sum_{t^{\prime}\in T_{N^{\prime}}}FiringFreq_{{\cal H}_{2}\cap DRS(N^{\prime})}(t^{\prime})=\\ \sum_{t^{\prime}\in T_{N^{\prime}}}\sum_{\{j\mid t^{\prime}\in Ena(M_{j}^{\prime}),\ M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}\Omega_{N^{\prime}}(t^{\prime},M_{j}^{\prime})=\varphi_{2}^{\prime}\Omega_{N^{\prime}}(t_{3}^{\prime},M_{2}^{\prime})+\varphi_{3}^{\prime}\Omega_{N^{\prime}}(t_{4}^{\prime},M_{3}^{\prime})=\frac{1}{4}\cdot 2+\frac{1}{4}\cdot 2=\frac{1}{2}+\frac{1}{2}=1$.

• •

The aggregate exit frequency of the discrete markings from ${\cal H}_{2}\cap DRS(N)$ is $ExitFreq({\cal H}_{2}\cap DRS(N))=\frac{\sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\varphi_{i}}{SJ({\cal H}_{2}\cap DRS(N))}=\frac{\varphi_{2}}{SJ(M_{2})}=\frac{1}{2}\cdot\frac{2}{1}=1$.

The aggregate exit frequency of the discrete markings from ${\cal H}_{2}\cap DRS(N^{\prime})$ is $ExitFreq({\cal H}_{2}\cap DRS(N^{\prime}))=\frac{\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}}{SJ({\cal H}_{2}\cap DRS(N^{\prime}))}=\frac{\varphi_{2}^{\prime}+\varphi_{3}^{\prime}}{SJ(M_{2}^{\prime})}=\frac{\varphi_{2}^{\prime}+\varphi_{3}^{\prime}}{SJ(M_{3}^{\prime})}=\left(\frac{1}{4}+\frac{1}{4}\right)\frac{2}{1}=1$.

• •

The aggregate mean potential fluid flow rate for the continuous place $q$ in the discrete markings from ${\cal H}_{2}\cap DRS(N)$ is $FluidFlow_{{\cal H}_{2}\cap DRS(N)}(q)=\sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\varphi_{i}RP({\cal H}_{2}\cap DRS(N))=\varphi_{2}RP(M_{2})=\frac{1}{2}(-2)=-1$.

The aggregate mean potential fluid flow rate for the continuous place $q$ in the discrete markings from ${\cal H}_{2}\cap DRS(N^{\prime})$ is $FluidFlow_{{\cal H}_{2}\cap DRS(N^{\prime})}(q)=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}RP({\cal H}_{2}\cap DRS(N^{\prime}))=(\varphi_{2}^{\prime}+\varphi_{3}^{\prime})RP(M_{2}^{\prime})=(\varphi_{2}^{\prime}+\varphi_{3}^{\prime})RP(M_{3}^{\prime})=\left(\frac{1}{4}+\frac{1}{4}\right)(-2)=-1$.

• •

The aggregate traversal frequency of the move from the discrete markings from ${\cal H}_{2}\cap DRS(N)$ to the discrete markings from ${\cal H}_{1}\cap DRS(N)$ is $TravFreq({\cal H}_{2}\cap DRS(N),{\cal H}_{1}\cap DRS(N))=\\ \sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\varphi_{i}RM({\cal H}_{2}\cap DRS(N),{\cal H}_{1}\cap DRS(N))=\varphi_{2}RM(M_{2},M_{1})=\frac{1}{2}\cdot 2=1$.

The aggregate traversal frequency of the move from the discrete markings from ${\cal H}_{2}\cap DRS(N^{\prime})$ to the discrete markings from ${\cal H}_{1}\cap DRS(N^{\prime})$ is $TravFreq({\cal H}_{2}\cap DRS(N^{\prime}),{\cal H}_{1}\cap DRS(N^{\prime}))=\\ \sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}\varphi_{j}^{\prime}RM({\cal H}_{2}\cap DRS(N^{\prime}),{\cal H}_{1}\cap DRS(N^{\prime}))=(\varphi_{2}^{\prime}+\varphi_{3}^{\prime})RM(M_{2}^{\prime},M_{1}^{\prime})=\\ (\varphi_{2}^{\prime}+\varphi_{3}^{\prime})RM(M_{3}^{\prime},M_{1}^{\prime})=\left(\frac{1}{4}+\frac{1}{4}\right)2=1$.

• •

The aggregate probability of the positive fluid level in the continuous place $q$ in the discrete markings from ${\cal H}_{2}\cap DRS(N)$ is $FluidLevel_{{\cal H}_{2}\cap DRS(N)}(q)=\sum_{\{i\mid M_{i}\in{\cal H}_{2}\cap DRS(N)\}}(\varphi_{i}-\ell_{i})=\varphi_{2}-\ell_{2}=\frac{1}{2}-\frac{1}{4}=\frac{1}{4}$.

The aggregate probability of the positive fluid level in the continuous place $q^{\prime}$ in the discrete markings from ${\cal H}_{2}\cap DRS(N^{\prime})$ is $FluidLevel_{{\cal H}_{2}\cap DRS(N^{\prime})}(q^{\prime})=\sum_{\{j\mid M_{j}^{\prime}\in{\cal H}_{2}\cap DRS(N^{\prime})\}}(\varphi_{j}^{\prime}-\ell_{j}^{\prime})=(\varphi_{2}^{\prime}-\ell_{2}^{\prime})+(\varphi_{3}^{\prime}-\ell_{3}^{\prime})=\left(\frac{1}{4}-\frac{1}{8}\right)+\left(\frac{1}{4}-\frac{1}{8}\right)=\frac{1}{8}+\frac{1}{8}=\frac{1}{4}$.

The following aggregate steady-state performance measures of $N$ do not coincide with those of $N^{\prime}$ for the equivalence class ${\cal H}_{2}$, since this index is based on the flow rates of continuous arcs from or to a continuous place. However, fluid bisimulation equivalence respects only the total difference between the flow rates of all the continuous arcs from a continuous place and the flow rates of all continuous arcs to the continuous place, and this difference is calculated only for a single discrete marking among several bisimilar ones. Nevertheless, we present these performance indices below with a goal to illustrate their calculation.

• •

The aggregate mean proportional flow rate across the continuous arcs from the continuous place $q$ to the transitions enabled in the discrete markings from ${\cal H}_{2}\cap DRS(N)$ is

$FluidFlowOut_{{\cal H}_{2}\cap DRS(N)}(q)=\sum_{t\in T_{N}}FluidFlow_{{\cal H}_{2}\cap DRS(N)}(q,t)=\\ \sum_{t\in T_{N}}\sum_{\{i\mid t\in Ena(M_{i}),\ M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\left(\ell_{i}\left(\frac{\sum_{u\in Ena(M)}R_{N}((u,q),M)}{\sum_{v\in Ena(M)}R_{N}((q,v),M)}-1\right)+\varphi_{i}\right)R_{N}((q,t),M)=\\ \left(\ell_{2}\left(\frac{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((q,t_{2}),M_{2})+\\ \left(\ell_{2}\left(\frac{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((q,t_{3}),M_{2})$.

We have $\frac{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}-1=\frac{R_{N}((t_{2},q),M_{2})+R_{N}((t_{3},q),M_{2})}{R_{N}((q,t_{2}),M_{2})+R_{N}((q,t_{3}),M_{2})}-1=\frac{1+2}{2+3}-1=-\frac{2}{5}$.

Thus, $\left(\ell_{2}\left(\frac{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((q,t_{2}),M_{2})+\\ \left(\ell_{2}\left(\frac{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((q,t_{3}),M_{2})=\left(\frac{1}{4}\left(-\frac{2}{5}\right)+\frac{1}{2}\right)2+\left(\frac{1}{4}\left(-\frac{2}{5}\right)+\frac{1}{2}\right)3=\frac{4}{5}+\frac{6}{5}=2$.

• •

The aggregate mean proportional flow rate across the continuous arcs to the continuous place $q$ from the transitions enabled in the discrete markings from ${\cal H}_{2}\cap DRS(N)$ is

$FluidFlowIn_{{\cal H}_{2}\cap DRS(N)}(q)=\sum_{t\in T_{N}}FluidFlow_{{\cal H}_{2}\cap DRS(N)}(t,q)=\\ \sum_{t\in T_{N}}\sum_{\{i\mid t\in Ena(M_{i}),\ M_{i}\in{\cal H}_{2}\cap DRS(N)\}}\left(\ell_{i}\left(\frac{\sum_{v\in Ena(M)}R_{N}((q,v),M)}{\sum_{u\in Ena(M)}R_{N}((u,q),M)}-1\right)+\varphi_{i}\right)R_{N}(((t,q),M)=\\ \left(\ell_{2}\left(\frac{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((t_{2},q),M_{2})+\\ \left(\ell_{2}\left(\frac{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((t_{3},q),M_{2})$.

We have $\frac{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}-1=\frac{R_{N}((q,t_{2}),M_{2})+R_{N}((q,t_{3}),M_{2})}{R_{N}((t_{2},q),M_{2})+R_{N}((t_{3},q),M_{2})}-1=\frac{2+3}{1+2}-1=\frac{2}{3}$.

Thus, $\left(\ell_{2}\left(\frac{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((t_{2},q),M_{2})+\\ \left(\ell_{2}\left(\frac{\sum_{v\in Ena(M_{2})}R_{N}((q,v),M_{2})}{\sum_{u\in Ena(M_{2})}R_{N}((u,q),M_{2})}-1\right)+\varphi_{2}\right)R_{N}((t_{3},q),M_{2})=\left(\frac{1}{4}\cdot\frac{2}{3}+\frac{1}{2}\right)1+\left(\frac{1}{4}\cdot\frac{2}{3}+\frac{1}{2}\right)2=\frac{2}{3}+\frac{4}{3}=2$.

11 Document preparation system

Let us consider an application example describing three different models of a document preparation system. The system receives (in an arbitrary order or in parallel) the collections of the text and graphics files as its inputs and writes them into the operative memory of a computer. The system then reads the (mixed) data from there and produces properly formatted output documents consisting of text and images. In general, it is supposed that the text file collections are transferred into the operative memory slower, but for longer time than the graphics ones. In detail, the low resolution graphics is transferred into the operative memory with the same speed as the high resolution one, but it takes less time than for the latter. The data from the operative memory is consumed for processing quicker, but for shorter time than the input file collections of any type. The operative memory capacity is supposed to be unlimited (for example, there exist some special mechanisms to ensure that the memory upper boundary can always be increased, such as using the page file, stored on a hard drive of the computer). Clearly, the lower boundary of the operative memory is zero. The diagram of the system is depicted in Figure 12.

The meaning of the actions that label the transitions of the LFSPNs which will specify the three models of the document preparation system is as follows. The action $tx$ represents writing the text files into the operative memory. The action $gr$ represents putting the graphics files into the operative memory. Particularly, the action $gl$ corresponds to writing the low resolution graphics while $gh$ specifies writing the high resolution graphics. The action $dt$ represents reading the data (consisting of the portions of the input text and images) from the operative memory. In each LFSPN, a single continuous place containing fluid will represent the operative memory with a data volume stored.

In Figure 13, the LFSPNs $N$ and $N^{\prime}$ specifying the standard document preparation system, as well as the LFSPN $N^{\prime\prime}$ representing the enhanced one that differentiates between the low and high resolution graphics, are presented. The rate of all transitions labeled with the action $tx$ is $1$, the rate of those labeled with $gr$ is $2$ and the rate of those labeled with $dt$ is $3$. Further, the rate of the transition with the label $gl$ is $\frac{3}{2}$ and the rate of that with the label $gh$ is $\frac{1}{2}$. The rate of the fluid flow along the continuous arcs from the transitions labeled with the action $tx$ is $1$ while that from the transitions labeled with $gr$ is $2$. Next, the fluid flow rate from the transitions with the label $gl$ or $gh$ is the same and equals $1$. The rate of the fluid flow along the continuous arcs to the transitions labeled with the action $dt$ is $7$.

We have $N\underline{\leftrightarrow}_{fl}N^{\prime}$. Since LFSPNs have an interleaving semantics due to the continuous time approach and the race condition applied to transition firings, the parallel execution of actions (here in $N$) is modeled by the sequential non-determinism (in $N^{\prime}$). Fluid bisimulation equivalence is an interleaving relation constructed in conformance with the LFSPNs semantics. In our application example, one can see that the “sequential” LFSPN $N^{\prime}$ may be replaced with the fluid bisimulation equivalent and structurally simpler “concurrent” LFSPN $N$, the latter having less transitions and arcs. Thus, the mentioned equivalence can be used not just to reduce behaviour of LFSPNs (as we have seen in the previous examples), but also to simplify their structure.

We have $DRS(N)=\{M_{1},M_{2},M_{3},M_{4}\}$, where $M_{1}=(1,1,0,0),\ M_{2}=(0,1,1,0),\ M_{3}=(1,0,0,1),\ M_{4}=(0,0,1,1)$; $DRS(N^{\prime})=\{M_{1}^{\prime},M_{2}^{\prime},M_{3}^{\prime},M_{4}^{\prime}\}$, where $M_{1}^{\prime}=(1,0,0,0),\ M_{2}^{\prime}=(0,1,0,0),\ M_{3}^{\prime}=(0,0,1,0),\ M_{4}^{\prime}=(0,0,0,1)$; and $DRS(N^{\prime\prime})=\{M_{1}^{\prime\prime},M_{2}^{\prime\prime},M_{3}^{\prime\prime},M_{4}^{\prime\prime},M_{5}^{\prime\prime},M_{6}^{\prime\prime}\}$, where $M_{1}^{\prime\prime}=(1,1,0,0,0),\ M_{2}^{\prime\prime}=(1,0,1,0,0),\ M_{3}^{\prime\prime}=(0,1,0,0,1),\ M_{4}^{\prime\prime}=(1,0,0,1,0),\ M_{5}^{\prime\prime}=(0,0,1,0,1),\ M_{6}^{\prime\prime}=(0,0,0,1,1)$.

In Figure 14, the discrete reachability graphs $DRG(N),\ DRG(N^{\prime})$ and $DRG(N^{\prime\prime})$ are depicted. Then it is clear that the discrete parts of the LFSPNs $N$ and $N^{\prime}$ have the same behaviour.

Let $N^{\prime\prime\prime}$ is an abstraction of $N^{\prime\prime}$ by assuming that the actions $gl$ and $gh$ coincide with the action $gr$. Then it holds $N\underline{\leftrightarrow}_{fl}N^{\prime}\underline{\leftrightarrow}_{fl}N^{\prime\prime\prime}$. In such a case, $DRS(N^{\prime\prime\prime})=\{M_{1}^{\prime\prime\prime},M_{2}^{\prime\prime\prime},M_{3}^{\prime\prime\prime},M_{4}^{\prime\prime\prime},M_{5}^{\prime\prime\prime},M_{6}^{\prime\prime\prime}\}$ coincides with $DRS(N^{\prime\prime})$ up to the trivial renaming bijection on the places. Further, $DRG(N^{\prime\prime\prime})$ coincides with $DRG(N^{\prime\prime})$ up to the analogous renaming the transitions.

Let ${\cal K}_{1}=\{M_{1}\},\ {\cal K}_{2}=\{M_{2}\},\ {\cal K}_{3}=\{M_{3}\},\ {\cal K}_{4}=\{M_{4}\}$ and ${\cal K}_{1}^{\prime}=\{M_{1}^{\prime}\},\ {\cal K}_{2}^{\prime}=\{M_{2}^{\prime}\},\ {\cal K}_{3}^{\prime}=\{M_{3}^{\prime}\},\ {\cal K}_{4}^{\prime}=\{M_{4}^{\prime}\}$, as well as ${\cal K}_{1}^{\prime\prime\prime}=\{M_{1}^{\prime\prime\prime}\},\ {\cal K}_{2}^{\prime\prime\prime}=\{M_{2}^{\prime\prime\prime},M_{4}^{\prime\prime\prime}\},\ {\cal K}_{3}^{\prime\prime\prime}=\{M_{3}^{\prime\prime\prime}\},\ {\cal K}_{4}^{\prime\prime\prime}=\{M_{5}^{\prime\prime\prime},M_{6}^{\prime\prime\prime}\}$. In Figure 15, the quotient (by $\underline{\leftrightarrow}_{fl}$) discrete reachability graphs $DRG_{\underline{\leftrightarrow}_{fl}}(N),\ DRG_{\underline{\leftrightarrow}_{fl}}(N^{\prime})$ and $DRG_{\underline{\leftrightarrow}_{fl}}(N^{\prime\prime\prime})$ are depicted. Obviously, $DRG_{\underline{\leftrightarrow}_{fl}}(N)\simeq DRG_{\underline{\leftrightarrow}_{fl}}(N^{\prime})\simeq DRG_{\underline{\leftrightarrow}_{fl}}(N^{\prime\prime\prime})$. Then it is clear that the discrete parts of the LFSPNs $N,\ N^{\prime}$ and $N^{\prime\prime\prime}$ have the same quotient behaviour. Thus, quotienting by fluid bisimulation equivalence can be used to substantially reduce behaviour of LFSPNs. It is also clear that the discrete parts of the LFSPNs $N$ and $N^{\prime}$ have the same complete and quotient behaviour.

The sojourn time average and variance vectors of $N^{\prime\prime\prime}$ are

[TABLE]

The complete and quotient sojourn time average and variance vectors of $N$ and $N^{\prime}$, as well as the quotient corresponding vectors of $N^{\prime\prime\prime}$, are

[TABLE]

[TABLE]

The TRM ${\bf Q}^{\prime\prime\prime}$ for $CTMC(N^{\prime\prime\prime})$, TPM ${\bf P}^{\prime\prime\prime}$ for $EDTMC(N^{\prime\prime\prime})$ and FRM ${\bf R}^{\prime\prime\prime}$ for the SFM of $N^{\prime\prime\prime}$ are

[TABLE]

The TRMs ${\bf Q},\ {\bf Q}_{\underline{\leftrightarrow}_{fl}},\ {\bf Q}^{\prime},\ {\bf Q}_{\underline{\leftrightarrow}_{fl}}^{\prime}$ and ${\bf Q}_{\underline{\leftrightarrow}_{fl}}^{\prime\prime\prime}$ for $CTMC(N),\ CTMC_{\underline{\leftrightarrow}_{fl}}(N),\ CTMC(N^{\prime}),\ CTMC_{\underline{\leftrightarrow}_{fl}}(N^{\prime})$

and $CTMC_{\underline{\leftrightarrow}_{fl}}(N^{\prime\prime\prime})$; TPMs ${\bf P},\ {\bf P}_{\underline{\leftrightarrow}_{fl}},\ {\bf P}^{\prime},\ {\bf P}_{\underline{\leftrightarrow}_{fl}}^{\prime}$ and ${\bf P}_{\underline{\leftrightarrow}_{fl}}^{\prime\prime\prime}$ for $EDTMC(N),\ EDTMC_{\underline{\leftrightarrow}_{fl}}(N),\\ EDTMC(N^{\prime}),\ EDTMC_{\underline{\leftrightarrow}_{fl}}(N^{\prime})$ and $EDTMC_{\underline{\leftrightarrow}_{fl}}(N^{\prime\prime\prime})$; as well as FRMs ${\bf R},\ {\bf R}_{\underline{\leftrightarrow}_{fl}},\ {\bf R}^{\prime},\ {\bf R}_{\underline{\leftrightarrow}_{fl}}^{\prime}$ and ${\bf R}_{\underline{\leftrightarrow}_{fl}}^{\prime\prime\prime}$ for the complete and quotient SFMs of $N,\ N^{\prime}$ and for the quotient SFM of $N^{\prime\prime\prime}$ are

[TABLE]

Thus, the respective discrete and continuous parts of the LFSPNs $N$ and $N^{\prime}$ have the same complete and quotient behaviour while $N^{\prime\prime\prime}$ has the same quotient one. Then it is enough to consider only LFSPN $N$ from now on.

The discrete markings of LFSPN $N$ are interpreted as follows: $M_{1}$: both the text and graphics file collections are written to the memory, $M_{2}$: the text file collection is resided in the memory and the graphics one is written to the memory, $M_{3}$: the graphics file collection is resided in the memory and the text one is written to the memory, $M_{4}$: the text and graphics file collections are resided in the memory and the data is read from there (if it is not empty).

We have $DRS^{-}(N)=\{M_{4}\},\ DRS^{0}(N)=\emptyset$ and $DRS^{+}(N)=\{M_{1},M_{2},M_{3}\}$.

The steady-state PMF for $CTMC(N)$ is

[TABLE]

Then the stability condition for the SFM of $N$ is fulfilled: $FluidFlow(q)=\sum_{i=1}^{4}\varphi_{i}RP(M_{i})=\frac{2}{9}\cdot 3+\frac{1}{9}\cdot 2+\frac{4}{9}\cdot 1+\frac{2}{9}(-7)=-\frac{2}{9}<0$.

For each eigenvalue $\gamma$ we must have |\gamma{\bf R}-{\bf Q}|=\left|\begin{array}[]{cccc}3(\gamma+1)&-1&-2&0\\ 0&2(\gamma+1)&0&-2\\ 0&0&\gamma+1&-1\\ -3&0&0&-7\gamma+3\end{array}\right|=-42\gamma^{4}-108\gamma^{3}-72\gamma^{2}-6\gamma=0; hence, $\gamma_{1}=0,\ \gamma_{2}=-1,\ \gamma_{3}=-\frac{1}{14}(11+\sqrt{93}),\ \gamma_{4}=-\frac{1}{14}(11-\sqrt{93})$.

The corresponding eigenvectors are the solutions of

[TABLE]

Then the eigenvectors are $v_{1}=\left(\frac{2}{9},\frac{1}{9},\frac{4}{9},\frac{2}{9}\right),\ v_{2}=(0,-1,2,0),\ v_{3}=\left(\frac{14}{3-\sqrt{93}},\frac{98}{(3-\sqrt{93})^{2}},\frac{392}{(3-\sqrt{93})^{2}},1\right),\\ v4=\left(\frac{14}{3+\sqrt{93}},\frac{98}{(3+\sqrt{93})^{2}},\frac{392}{(3+\sqrt{93})^{2}},1\right)$.

Since $\varphi=F(\infty)=a_{1}v_{1}$, we have $F(x)=\varphi+a_{2}e^{\gamma_{2}x}v_{2}+a_{3}e^{\gamma_{3}x}v_{3}+a_{4}e^{\gamma_{4}x}v_{4}$ and $a_{1}=1$. Since $\forall M_{l}\in DRS^{+}(N)\ F_{l}(0)=\varphi_{l}+a_{2}v_{2l}+a_{3}v_{3l}+a_{4}v_{4l}=0$ and $DRS^{+}(N)=\{M_{1},M_{2},M_{3}\}$, we have the following linear equation system: \left\{\begin{array}[]{l}\varphi_{1}+a_{2}v_{21}+a_{3}v_{31}+a_{4}v_{41}=\frac{2}{9}+\frac{14}{3-\sqrt{93}}a_{3}+\frac{14}{3+\sqrt{93}}a_{4}=0\\ \varphi_{2}+a_{2}v_{22}+a_{3}v_{32}+a_{4}v_{42}=\frac{1}{9}-a_{2}+\frac{98}{(3-\sqrt{93})^{2}}a_{3}+\frac{98}{(3+\sqrt{93})^{2}}a_{4}=0\\ \varphi_{3}+a_{2}v_{23}+a_{3}v_{33}+a_{4}v_{43}=\frac{4}{9}+2a_{2}+\frac{392}{(3-\sqrt{93})^{2}}a_{3}+\frac{392}{(3+\sqrt{93})^{2}}a_{4}=0\end{array}\right..

By solving the system, we get $a_{2}=0,\ a_{3}=\frac{2(31-3\sqrt{93})}{93(3+\sqrt{93})},\ a_{4}=-\frac{2(10+\sqrt{93})}{21\sqrt{93}}$. Thus, $F(x)=\left(\frac{2}{9},\frac{1}{9},\frac{4}{9},\frac{2}{9}\right)+\frac{2(31-3\sqrt{93})}{93(3+\sqrt{93})}e^{-\frac{1}{14}(11+\sqrt{93})x}\left(\frac{14}{3-\sqrt{93}},\frac{98}{(3-\sqrt{93})^{2}},\frac{392}{(3-\sqrt{93})^{2}},1\right)\!-\!\frac{2(10+\sqrt{93})}{21\sqrt{93}}e^{-\frac{1}{14}(11-\sqrt{93})x}\left(\frac{14}{3+\sqrt{93}},\frac{98}{(3+\sqrt{93})^{2}},\frac{392}{(3+\sqrt{93})^{2}},1\right)$.

Then the steady-state fluid PDF for the SFM of $N$ is

[TABLE]

The steady-state fluid probability density function for the SFM of $N$ is

[TABLE]

The steady-state buffer empty probability for the SFM of $N$ is

[TABLE]

In Figure 16, the plots of the elements $F_{1},F_{2},F_{3},F_{4}$ of the steady-state fluid PDF $F=(F_{1},F_{2},F_{3},F_{4})$ for the SFM of $N$, as functions of $x$, are depicted.

We can now calculate some steady-state performance measures for the document preparation system.

• •

The fraction of time when both the text and graphics file collections are written to the memory is

[TABLE]

• •

The average number of the text file collections received per unit of time is

[TABLE]

• •

The throughput of the system is

[TABLE]

• •

The probability that the memory is not empty is

[TABLE]

• •

The probability that the operative memory contains at least $5$ Mb data is

[TABLE]

Since $N\underline{\leftrightarrow}_{fl}N^{\prime}\underline{\leftrightarrow}_{fl}N^{\prime\prime\prime}$, the LFSPNs $N,\ N^{\prime}$ and $N^{\prime\prime\prime}$ satisfy the same formulas of $HML_{flt}$ (with the identical interpretation values) and $HML_{flb}$. For instance, consider the following formulas for LFSPN $N$.

We have $[\![\langle tx\rangle\langle gr\rangle\top]\!]_{flt}(M_{N},\frac{1}{3}\circ\frac{1}{2}\circ\frac{1}{3},3\circ 2\circ(-7))=PT(t_{1}t_{2})=\frac{1}{3}\cdot 1=\frac{1}{3}$, i.e. the value $\frac{1}{3}$ is the probability that the text files are written into the operative memory with the potential flow rate $3$ during the exponentially distributed time period with the average $\frac{1}{3}$; then the graphics files are written into the memory with the potential flow rate $2$ during the exponentially distributed time period with the average $\frac{1}{2}$; finally, the data is read from the memory with the potential flow rate $-7$ for the exponentially distributed time period with the average $\frac{1}{3}$.

Further, it holds $M_{N}\models_{flb}\wr_{3}\wedge(\langle tx\rangle_{1}\top\vee\langle gr\rangle_{2}\top)$, i.e. it is valid that the text files are written into the operative memory with the potential flow rate $3$ during the exponentially distributed time period with the rate $1$ or the graphics files are written into the memory with the same potential flow rate $3$ during the exponentially distributed time period with the rate $2$.

12 Conclusion

In this paper, we have defined two behavioural equivalences that preserve the qualitative and quantitative behavior of LFSPNs, related to both their discrete part (labeled CTSPNs and the underlying CTMCs) and continuous part (the associated SFMs). We have proposed on LFSPNs a linear-time relation of fluid trace equivalence and a branching-time relation of fluid bisimulation equivalence. Both equivalences respect functional activity, stochastic timing and fluid flow in the behaviour of LFSPNs. We have demonstrated that fluid trace equivalence preserves average potential fluid change volume for the transition sequences of each given length. We have proven that fluid bisimulation equivalence implies fluid trace equivalence and the reverse implication does not hold in general. We have explained how to reduce the discrete reachability graphs and underlying CTMCs of LFSPNs with respect to fluid bisimulation equivalence by applying the technique that builds the quotients of the respective labeled transition systems by the largest fluid bisimulation. We have defined the quotients of the probability functions by fluid bisimulation equivalence to describe the quotient associated SFMs. We have characterized logically fluid trace and bisimulation equivalences with two novel fluid modal logics $HML_{flt}$ and $HML_{flb}$. The characterizations give rise to better understanding of basic features of the equivalences. According to [2], we have demonstrated that the fluid equivalences are reasonable notions, by constructing their natural and pleasant modal characterizations. In addition, they offer a possibility for the logical reasoning on resemblance of the fluid behaviour, while before it was only possible in the operational manner. For example, let $N$ be one of the fluid (trace of bisimulation) equivalent LFSPNs that model the production line mentioned in Section 1. In the initial discrete marking $M_{N}$, we now can specify and verify formally the properties described there: the probability given by the interpretation $[\![\langle f_{1}\rangle\langle f_{2}\rangle\top]\!]_{flt}(M_{N},s_{1}s_{2}s_{3},r_{1}r_{2}r_{3})$ in $HML_{flt}$ and the validity of the satisfaction $M_{N}\models_{flb}\wr_{r_{1}}\wedge(\langle f_{1}\rangle_{\lambda_{1}}\top\vee\langle f_{2}\rangle_{\lambda_{2}}\top)$ in $HML_{flb}$. We have proven that fluid bisimulation equivalence preserves the qualitative and stationary quantitative behaviour, hence, it guarantees that the functionality and performance measures of the equivalent systems coincide. We have presented a case study of the three LFSPNs, all modeling the document preparation system, with intention to show how fluid bisimulation equivalence can be used to simplify the LFSPNs structure and behaviour.

In the future, we plan to define a fluid place bisimulation relation that connects “similar” continuous places of LFSPNs, like place bisimulations [7, 6, 70, 71, 72] relate discrete places of (standard) Petri nets. The lifting of the relation to the discrete-continuous LFSPN markings (with discrete markings treated as the multisets of places) will respect both the fluid distribution among the related continuous places and the rates of fluid flow through them. For this purpose, we should introduce a novel notion of the multiset analogue with non-negative real-valued multiplicities of the elements. While multiset is a mapping from a countable set to all natural numbers, we need a more sophisticated mapping from the set of continuous places to all non-negative real numbers, corresponding to the associated fluid levels. Such an extension of the multiset notion may use the results of [22, 69], concerning hybrid sets (the multiplicities of the elements are arbitrary integers) and fuzzy multisets (the multiplicities belong to the interval [0;1]). In this way, both the initial amount of fluid and its transit flow rate in each discrete marking may be distributed among several continuous places of an LFSPN, such that all of them are bisimilar to a particular continuous place of the equivalent LFSPN. The interesting point here is that fluid distributed among several bisimilar continuous places should be taken as the fluid contained in a single continuous place, resulting from aggregating those “constituent” continuous places with the use of fluid place bisimulation. Then the fluid level in the “aggregate” continuous place will be a sum of the fluid levels in the “constituent” continuous places. The probability density function for the sum of random variables representing the fluid levels in the “constituent” continuous places is defined via convolution operation. In this approach, we should avoid or treat correctly the situations when the fluid flow in the “aggregate” continuous place becomes suddenly non-continuous. This happens when some of the “constituent” continuous places are emptied while the others still contain a positive amount of fluid. Obviously, such a discontinuity is a result of applying the aggregation since it is not caused by either reaching the lower fluid boundary (zero fluid level) or change of the current discrete marking.

We assume that summation of the fluid levels in the continuous places may be implemented with the constructions proposed in [43] for extended FSPNs (EFSPNs). EFSPNs have special deterministic fluid jump arcs that are used to transfer a deterministic amount of fluid from one continuous place to another via intermediate stochastic transitions connecting both places (deterministic fluid transfer). Analogously, random fluid jump arcs in EFSPNs are used to transfer a random amount of fluid from one continuous place to another (random fluid transfer). We can also use fluid transitions, mentioned in [43] as a direction for future development of the FSPNs formalism. Fluid transitions that transfer fluid from their input to their output continuous places are used to implement fluid volume conservation. If one of the input continuous places of a fluid transition becomes empty (i.e. the lower fluid boundary is reached) then the rate of the transition should change in a certain way. The continuous arcs between continuous places and fluid transitions may have multiplicities that multiply (change according to a factor) the fluid flow along the arcs. Fluid transitions may be controlled by a discrete marking, using the guard functions associated with them or applying the inhibitor and test arcs, i.e. by the constructions that do not affect discrete markings.

Further, we intend to apply to LFSPNs an analogue of the effective reduction technique based on the place bisimulations of Petri nets [7, 6]. In this way, we shall merge several equivalent continuous places and, in some cases, the transitions between them. This should result in the significant reductions of LFSPNs. The number of continuous places in an LFSPN impacts drastically the complexity of its solution. The analytical solution is normally possible for just a few continuous places (or even only for one). In all other cases, when modeling realistic large and complex systems, we have to apply numerical techniques to solve systems of partial differential equations, or the method of simulation. Hence, the reduction of the number of continuous places accomplished with the place bisimulation merging appears to be even more important for LFSPNs than for Petri nets.