General information
Latest issue
Impact factor

Search papers
Search references

Latest issue
Current issues
Archive issues
What is RSS

Sib. Èlektron. Mat. Izv.:

Personal entry:
Save password
Forgotten password?

Sib. Èlektron. Mat. Izv., 2019, Volume 16, Pages 826–862 (Mi semr1097)  

Mathematical logic, algebra and number theory

Logical characterization of fluid equivalences

I. V. Tarasyuka, P. Buchholzb

a A.P. Ershov Institute of Informatics Systems, Siberian Branch of the Russian Academy of Sciences, 6, Acad. Lavrentiev ave., Novosibirsk, 630090, Russian Federation
b Faculty of Computer Science, Technical University of Dortmund, 16, Otto-Hahn-Str., Dortmund, 44227, Germany

Abstract: 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.

Funding Agency Grant Number
Deutsche Forschungsgemeinschaft BE 1267/14-1
The work was supported in part by Deutsche Forschungsgemeinschaft (DFG) under grant BE 1267/14-1.


Full text: PDF file (414 kB)
References: PDF file   HTML file

Bibliographic databases:

UDC: 519.217.2, 519.681.2, 519.681.3
MSC: 60J27, 60K15, 68Q85, 68Q87
Received May 10, 2018, published June 11, 2019

Citation: I. V. Tarasyuk, P. Buchholz, “Logical characterization of fluid equivalences”, Sib. Èlektron. Mat. Izv., 16 (2019), 826–862

Citation in format AMSBIB
\by I.~V.~Tarasyuk, P.~Buchholz
\paper Logical characterization of fluid equivalences
\jour Sib. \`Elektron. Mat. Izv.
\yr 2019
\vol 16
\pages 826--862

Linking options:

    SHARE: FaceBook Twitter Livejournal

    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Number of views:
    This page:13
    Full text:3

    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2019