1,720,991 research outputs found
SOS specifications for uniformly continuous operators
No full textBehavioral metric semantics provide formal notions to compare probabilistic systems, giving a notion of behavioral distance characterizing how far the behavior of two systems is apart. Compositional reasoning over probabilistic systems with respect to behavioral metric semantics requires the language operators to be uniformly continuous, which ensures that a limited change in the behavior of a subsystem implies a smooth and limited change in the behavior of the whole system. We consider a hierarchy of uniform continuity properties for process algebra operators and, for each of these properties, we propose a Structural Operational Semantics specification format (namely a set of syntactical constraints on the form of the SOS rules) ensuring that the property is satisfied by construction by all operators captured by the format
Modal Decomposition on Nondeterministic Probabilistic Processes
Full text linkWe propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes.
The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition.
By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity
Logical Characterization of Bisimulation Metrics
Full text linkBisimulation metrics provide a robust and accurate approach to study the behavior of nondeterministic probabilistic processes. In this paper, we propose a logical characterization of bisimulation metrics based on a simple probabilistic variant of the Hennessy-Milner logic. Our approach is based on the novel notions of mimicking formulae and distance between formulae. The former are a weak version of the well known characteristic formulae and allow us to characterize also (ready) probabilistic simulation and probabilistic bisimilarity. The latter is a 1-bounded pseudometric on formulae that mirrors the Hausdorff and Kantorovich lifting the defining bisimilarity pseudometric. We show that the distance between two processes equals the distance between their own mimicking formulae
SOS specifications of probabilistic systems by uniformly continuous operators
Full text linkCompositional reasoning over probabilistic systems wrt. behavioral metric semantics requires the language operators to be uniformly continuous. We study which SOS specifications define uniformly continuous operators wrt. bisimulation metric semantics. We propose an expressive specification format that allows us to specify operators of any given modulus of continuity. Moreover, we provide a method that allows to derive from any given specification the modulus of continuity of its operators
Fixed-point characterization of compositionality properties of probabilistic processes combinators
Full text linkBisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric compositionality property. The compositionality property of an operator is defined as its modulus of continuity which gives the relative increase of the distance between processes when they are combined by that operator. The compositionality property of an operator is computed by recursively counting how many times the combined processes are copied along their evolution. The compositionality properties allow to derive an upper bound on the distance between processes by purely inspecting the operators used to specify those processes
A general SOS theory for the specification of probabilistic transition systems
Full text linkThis article focuses on the formalization of the structured operational semantics approach for languages with primitives that introduce probabilistic and non-deterministic behavior. We define a general theoretic framework and present the ntμfθ/ntμxθ rule format that guarantees that bisimulation equivalence (in the probabilistic setting) is a congruence for any operator defined in this format. We show that the bisimulation is fully abstract w.r.t. the ntμfθ/ntμxθ format and (possibilistic) trace equivalence in the sense that bisimulation is the coarsest congruence included in trace equivalence for any operator definable within the ntμfθ/ntμxθ format (in other words, bisimulation is the smallest congruence relation guaranteed by the format). We also provide a conservative extension theorem and show that languages that include primitives for exponentially distributed time behavior (such as IMC and Markov automata based language) fit naturally within our framework.Fil: D'argenio, Pedro Ruben. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Gebler, Daniel. Vrije Universiteit Amsterdam; Países BajosFil: Lee, Matias David. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física. Sección Ciencias de la Computación; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentin
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
