Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userModal Characterisations of Behavioural Pseudometrics
198
0
0.0
(
0
)
Added by
Yuxin Deng
Publication date
2015
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
For the model of probabilistic labelled transition systems that allow for the co-existence of nondeterminism and probabilities, we present two notions of bisimulation metrics: one is state-based and the other is distribution-based. We provide a sound and complete modal characterisation for each of them, using real-valued modal logics based on the Hennessy-Milner logic. The logic for characterising the state-based metric is much simpler than an earlier logic by Desharnais et al. as it uses only two non-expansive operators rather than the general class of non-expansive operators.
rate research
Read More
Many behavioural equivalences or preorders for probabilistic processes involve a lifting operation that turns a relation on states into a relation on distributions of states. We show that several existing proposals for lifting relations can be reconciled to be different presentations of essentially the same lifting operation. More interestingly, this lifting operation nicely corresponds to the Kantorovich metric, a fundamental concept used in mathematics to lift a metric on states to a metric on distributions of states, besides the fact the lifting operation is related to the maximum flow problem in optimisation theory. The lifting operation yields a neat notion of probabilistic bisimulation, for which we provide logical, metric, and algorithmic characterisations. Specifically, we extend the Hennessy-Milner logic and the modal mu-calculus with a new modality, resulting in an adequate and an expressive logic for probabilistic bisimilarity, respectively. The correspondence of the lifting operation and the Kantorovich metric leads to a natural characterisation of bisimulations as pseudometrics which are post-fixed points of a monotone function. We also present an on the fly algorithm to check if two states in a finitary system are related by probabilistic bisimilarity, exploiting the close relationship between the lifting operation and the maximum flow problem.
The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial structures, such as finite graphs and digital images, with applications in various case studies including medical image analysis. These recent developments required a generalisation step, from topological spaces to closure spaces. In this work we initiate the study of bisimilarity and minimisation algorithms that are consistent with the closure spaces semantics. For this purpose we employ coalgebraic models. We present a coalgebraic definition of bisimilarity for quasi-discrete models, which is adequate with respect to a spatial logic with reachability operators, complemented by a free and open-source minimisation tool for finite models. We also discuss the non-quasi-discrete case, by providing a generalisation of the well-known set-theoretical notion of topo-bisimilarity, and a categorical definition, in the same spirit as the coalgebraic rendition of neighbourhood frames, but employing the covariant power set functor, instead of the contravariant one. We prove its adequacy with respect to infinitary modal logic.
We propose a process calculus, named AbC, to study the behavioural theory of interactions in collective-adaptive systems by relying on attribute-based communication. An AbC system consists of a set of parallel components each of which is equipped with a set of attributes. Communication takes place in an implicit multicast fashion, and interaction among components is dynamically established by taking into account connections as determined by predicates over their attributes. The structural operational semantics of AbC is based on Labeled Transition Systems that are also used to define bisimilarity between components. Labeled bisimilarity is in full agreement with a barbed congruence, defined by simple basic observables and context closure. The introduced equivalence is used to study the expressiveness of AbC in terms of encoding broadcast channel-based interactions and to establish formal relationships between system descriptions at different levels of abstraction.
Let $X$, $Y$ be sets and let $Phi$, $Psi$ be mappings with the domains $X^{2}$ and $Y^{2}$ respectively. We say that $Phi$ is combinatorially similar to $Psi$ if there are bijections $f colon Phi(X^2) to Psi(Y^{2})$ and $g colon Y to X$ such that $Psi(x, y) = f(Phi(g(x), g(y)))$ for all $x$, $y in Y$. It is shown that the semigroups of binary relations generated by sets ${Phi^{-1}(a) colon a in Phi(X^{2})}$ and ${Psi^{-1}(b) colon b in Psi(Y^{2})}$ are isomorphic for combinatorially similar $Phi$ and $Psi$. The necessary and sufficient conditions under which a given mapping is combinatorially similar to a pseudometric, or strongly rigid pseudometric, or discrete pseudometric are found. The algebraic structure of semigroups generated by ${d^{-1}(r) colon r in d(X^{2})}$ is completely described for nondiscrete, strongly rigid pseudometrics and, also, for discrete pseudometrics $d colon X^{2} to mathbb{R}$.
This paper studies the quantitative refinements of Abramskys applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value $lambda$-calculus with a linear type system that can express programs sensitivity, enriched with algebraic operations emph{`a la} Plotkin and Power. To do so a general, abstract framework for studying behavioural relations taking values over quantales is defined according to Lawveres analysis of generalised metric spaces. Barrs notion of relator (or lax extension) is then extended to quantale-valued relations adapting and extending results from the field of monoidal topology. Abstract notions of quantale-valued effectful applicative similarity and bisimilarity are then defined and proved to be a compatible generalised metric (in the sense of Lawvere) and pseudometric, respectively, under mild conditions.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
