RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
 General information Latest issue Archive Impact factor Search papers Search references RSS Latest issue Current issues Archive issues What is RSS

 Sib. Èlektron. Mat. Izv.: Year: Volume: Issue: Page: Find

 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.

DOI: https://doi.org/10.33048/semi.2019.16.055

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
Language:

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

Citation in format AMSBIB
\Bibitem{TarBuc19} \by I.~V.~Tarasyuk, P.~Buchholz \paper Logical characterization of fluid equivalences \jour Sib. \Elektron. Mat. Izv. \yr 2019 \vol 16 \pages 826--862 \mathnet{http://mi.mathnet.ru/semr1097} \crossref{https://doi.org/10.33048/semi.2019.16.055} \isi{http://gateway.isiknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&DestLinkType=FullRecord&DestApp=ALL_WOS&KeyUT=000471695600001} `