Logical characterization of fluid equivalences
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 16 (2019), pp. 826-862

Voir la notice de l'article provenant de la source Math-Net.Ru

We investigate fluid equivalences that allow one to compare and reduce behaviour of labeled fluid stochastic Petri nets (LFSPNs) with a single continuous place while preserving their discrete and continuous properties. We propose 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, such as functional activity, stochastic timing and fluid flow. We consider the LFSPNs whose continuous markings have no influence to the discrete ones, i.e. every discrete marking determines completely both the set of enabled transitions, their firing rates and the fluid flow rates of the incoming and outgoing arcs for each continuous place. Moreover, we require that the discrete part of the LFSPNs should be 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 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 characterizations guarantee that two LFSPNs are fluid (trace or bisimulation) equivalent iff they satisfy the same formulas of the respective logic, i.e. they are logically equivalent. The results imply operational characterizations of the logical equivalences.
Keywords: labeled fluid stochastic Petri net, continuous time stochastic Petri net, continuous time Markov chain, stochastic fluid model, transient and stationary behaviour, fluid trace and bisimulation equivalences, fluid modal logic, logical and operational characterizations.
@article{SEMR_2019_16_a13,
     author = {I. V. Tarasyuk and P. Buchholz},
     title = {Logical characterization of fluid equivalences},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {826--862},
     publisher = {mathdoc},
     volume = {16},
     year = {2019},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/}
}
TY  - JOUR
AU  - I. V. Tarasyuk
AU  - P. Buchholz
TI  - Logical characterization of fluid equivalences
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2019
SP  - 826
EP  - 862
VL  - 16
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/
LA  - en
ID  - SEMR_2019_16_a13
ER  - 
%0 Journal Article
%A I. V. Tarasyuk
%A P. Buchholz
%T Logical characterization of fluid equivalences
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2019
%P 826-862
%V 16
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/
%G en
%F SEMR_2019_16_a13
I. V. Tarasyuk; P. Buchholz. Logical characterization of fluid equivalences. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 16 (2019), pp. 826-862. http://geodesic.mathdoc.fr/item/SEMR_2019_16_a13/