-
Universal Quantitative Algebra for Fuzzy Relations and Generalised Metric Spaces
Authors:
Matteo Mio,
Ralph Sarkis,
Valeria Vignudelli
Abstract:
We present a generalisation of the theory of quantitative algebras of Mardare, Panangaden and Plotkin where (i) the carriers of quantitative algebras are not restricted to be metric spaces and can be arbitrary fuzzy relations or generalised metric spaces, and (ii) the interpretations of the algebraic operations are not required to be nonexpansive. Our main results include: a novel sound and comple…
▽ More
We present a generalisation of the theory of quantitative algebras of Mardare, Panangaden and Plotkin where (i) the carriers of quantitative algebras are not restricted to be metric spaces and can be arbitrary fuzzy relations or generalised metric spaces, and (ii) the interpretations of the algebraic operations are not required to be nonexpansive. Our main results include: a novel sound and complete proof system, the proof that free quantitative algebras always exist, the proof of strict monadicity of the induced Free-Forgetful adjunction, the result that all monads (on fuzzy relations) that lift finitary monads (on sets) admit a quantitative equational presentation.
△ Less
Submitted 24 September, 2023; v1 submitted 27 April, 2023;
originally announced April 2023.
-
Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
Authors:
Matteo Mio,
Ralph Sarkis,
Valeria Vignudelli
Abstract:
The framework of quantitative equational logic has been successfully applied to reason about algebras whose carriers are metric spaces and operations are nonexpansive. We extend this framework in two orthogonal directions: algebras endowed with generalised metric space structures, and operations being nonexpansive up to a lifting. We apply our results to the algebraic axiomatisation of the Łukaszy…
▽ More
The framework of quantitative equational logic has been successfully applied to reason about algebras whose carriers are metric spaces and operations are nonexpansive. We extend this framework in two orthogonal directions: algebras endowed with generalised metric space structures, and operations being nonexpansive up to a lifting. We apply our results to the algebraic axiomatisation of the Łukaszyk--Karmowski distance on probability distributions, which has recently found application in the field of representation learning on Markov processes.
△ Less
Submitted 22 January, 2022;
originally announced January 2022.
-
Combining nondeterminism, probability, and termination: equational and metric reasoning
Authors:
Matteo Mio,
Ralph Sarkis,
Valeria Vignudelli
Abstract:
We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads, providing equational reasoning tools for establishing equivalences and distances of programs.
We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads, providing equational reasoning tools for establishing equivalences and distances of programs.
△ Less
Submitted 21 April, 2021; v1 submitted 1 December, 2020;
originally announced December 2020.
-
Monads and Quantitative Equational Theories for Nondeterminism and Probability
Authors:
Matteo Mio,
Valeria Vignudelli
Abstract:
The monad of convex sets of probability distributions is a well-known tool for modelling the combination of nondeterministic and probabilistic computational effects. In this work we lift this monad from the category of sets to the category of metric spaces, by means of the Hausdorff and Kantorovich metric liftings. Our main result is the presentation of this lifted monad in terms of the quantitati…
▽ More
The monad of convex sets of probability distributions is a well-known tool for modelling the combination of nondeterministic and probabilistic computational effects. In this work we lift this monad from the category of sets to the category of metric spaces, by means of the Hausdorff and Kantorovich metric liftings. Our main result is the presentation of this lifted monad in terms of the quantitative equational theory of convex semilattices, using the framework of quantitative algebras recently introduced by Mardare, Panangaden and Plotkin.
△ Less
Submitted 15 May, 2020;
originally announced May 2020.
-
Proof Theory of Riesz Spaces and Modal Riesz Spaces
Authors:
Christophe Lucas,
Matteo Mio
Abstract:
We design hypersequent calculus proof systems for the theories of Riesz spaces and modal Riesz spaces and prove the key theorems: soundness, completeness and cut elimination. These are then used to obtain completely syntactic proofs of some interesting results concerning the two theories. Most notably, we prove a novel result: the theory of modal Riesz spaces is decidable. This work has applicatio…
▽ More
We design hypersequent calculus proof systems for the theories of Riesz spaces and modal Riesz spaces and prove the key theorems: soundness, completeness and cut elimination. These are then used to obtain completely syntactic proofs of some interesting results concerning the two theories. Most notably, we prove a novel result: the theory of modal Riesz spaces is decidable. This work has applications in the field of logics of probabilistic programs since modal Riesz spaces provide the algebraic semantics of the Riesz modal logic underlying the probabilistic mu-calculus.
△ Less
Submitted 16 February, 2022; v1 submitted 23 April, 2020;
originally announced April 2020.
-
Probabilistic logics based on Riesz spaces
Authors:
Robert Furber,
Radu Mardare,
Matteo Mio
Abstract:
We introduce a novel real-valued endogenous logic for expressing properties of probabilistic transition systems called Riesz modal logic. The design of the syntax and semantics of this logic is directly inspired by the theory of Riesz spaces, a mature field of mathematics at the intersection of universal algebra and functional analysis. By using powerful results from this theory, we develop the du…
▽ More
We introduce a novel real-valued endogenous logic for expressing properties of probabilistic transition systems called Riesz modal logic. The design of the syntax and semantics of this logic is directly inspired by the theory of Riesz spaces, a mature field of mathematics at the intersection of universal algebra and functional analysis. By using powerful results from this theory, we develop the duality theory of the Riesz modal logic in the form of an algebra-to-coalgebra correspondence. This has a number of consequences including: a sound and complete axiomatization, the proof that the logic characterizes probabilistic bisimulation and other convenient results such as completion theorems. This work is intended to be the basis for subsequent research on extensions of Riesz modal logic with fixed-point operators.
△ Less
Submitted 24 January, 2020; v1 submitted 22 March, 2019;
originally announced March 2019.
-
Monadic Second Order Logic with Measure and Category Quantifiers
Authors:
Matteo Mio,
Michał Skrzypczak,
Henryk Michalewski
Abstract:
We investigate the extension of Monadic Second Order logic, interpreted over infinite words and trees, with generalized "for almost all" quantifiers interpreted using the notions of Baire category and Lebesgue measure.
We investigate the extension of Monadic Second Order logic, interpreted over infinite words and trees, with generalized "for almost all" quantifiers interpreted using the notions of Baire category and Lebesgue measure.
△ Less
Submitted 9 April, 2018; v1 submitted 15 February, 2017;
originally announced February 2017.
-
On the Regular Emptiness Problem of Subzero Automata
Authors:
Henryk Michalewski,
Matteo Mio,
Mikołaj Bojańczyk
Abstract:
Subzero automata is a class of tree automata whose acceptance condition can express probabilistic constraints. Our main result is that the problem of determining if a subzero automaton accepts some regular tree is decidable.
Subzero automata is a class of tree automata whose acceptance condition can express probabilistic constraints. Our main result is that the problem of determining if a subzero automaton accepts some regular tree is decidable.
△ Less
Submitted 10 August, 2016;
originally announced August 2016.
-
On the Problem of Computing the Probability of Regular Sets of Trees
Authors:
Henryk Michalewski,
Matteo Mio
Abstract:
We consider the problem of computing the probability of regular languages of infinite trees with respect to the natural coin-flip** measure. We propose an algorithm which computes the probability of languages recognizable by \emph{game automata}. In particular this algorithm is applicable to all deterministic automata. We then use the algorithm to prove through examples three properties of measu…
▽ More
We consider the problem of computing the probability of regular languages of infinite trees with respect to the natural coin-flip** measure. We propose an algorithm which computes the probability of languages recognizable by \emph{game automata}. In particular this algorithm is applicable to all deterministic automata. We then use the algorithm to prove through examples three properties of measure: (1) there exist regular sets having irrational probability, (2) there exist comeager regular sets having probability $0$ and (3) the probability of \emph{game languages} $W_{i,k}$, from automata theory, is $0$ if $k$ is odd and is $1$ otherwise.
△ Less
Submitted 6 October, 2015;
originally announced October 2015.
-
Łukasiewicz μ-calculus
Authors:
Matteo Mio,
Alex Simpson
Abstract:
The paper explores properties of the Łukasiewicz μ-calculus, or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with $n$ variables, define monotone piecewise linear functions from $[0, 1]^n$ to $[0, 1]$. Two effective procedures for calculating the output of Łμ terms on ration…
▽ More
The paper explores properties of the Łukasiewicz μ-calculus, or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with $n$ variables, define monotone piecewise linear functions from $[0, 1]^n$ to $[0, 1]$. Two effective procedures for calculating the output of Łμ terms on rational inputs are presented. We then consider the Łukasiewicz modal μ-calculus, which is obtained by adding box and diamond modalities to Łμ. Alternatively, it can be viewed as a generalization of Kozen's modal μ-calculus adapted to probabilistic nondeterministic transition systems (PNTS's). We show how properties expressible in the well-known logic PCTL can be encoded as Łukasiewicz modal μ-calculus formulas. We also show that the algorithms for computing values of Łukasiewicz μ-calculus terms provide automatic (albeit impractical) methods for verifying Łukasiewicz modal μ-calculus properties of finite rational PNTS's.
△ Less
Submitted 3 October, 2015;
originally announced October 2015.
-
Proceedings Tenth International Workshop on Fixed Points in Computer Science
Authors:
Ralph Matthes,
Matteo Mio
Abstract:
This volume contains the proceedings of the Tenth International Workshop on Fixed Points in Computer Science (FICS 2015) which took place on September 11th and 12th, 2015 in Berlin, Germany, as a satellite event of the conference Computer Science Logic (CSL 2015).
Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and ass…
▽ More
This volume contains the proceedings of the Tenth International Workshop on Fixed Points in Computer Science (FICS 2015) which took place on September 11th and 12th, 2015 in Berlin, Germany, as a satellite event of the conference Computer Science Logic (CSL 2015).
Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and associated reasoning techniques. The construction and properties of fixed points have been investigated in many different settings such as: design and implementation of programming languages, logics, verification, databases. The aim of this workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points.
Each of the 11 contributed papers of this volume were evaluated by three or four reviewers. Some of the papers were re-reviewed after revision.
Additionally, this volume contains the abstracts of the FICS 2015 invited talks given by Bartek Klin and James Worrell.
△ Less
Submitted 9 September, 2015;
originally announced September 2015.
-
Upper-Expectation Bisimilarity and Real-valued Modal Logics
Authors:
Matteo Mio
Abstract:
Several notions of bisimulation relations for probabilistic non-deterministic transition systems have been considered in the literature. We consider a novel testing-based behavioral equivalence called upper-expectation bisimilarity and develop its theory using standard results from linear algebra and functional analysis. We show that, for a wide class of systems, our new notion coincides with Sega…
▽ More
Several notions of bisimulation relations for probabilistic non-deterministic transition systems have been considered in the literature. We consider a novel testing-based behavioral equivalence called upper-expectation bisimilarity and develop its theory using standard results from linear algebra and functional analysis. We show that, for a wide class of systems, our new notion coincides with Segala's convex bisimilarity. We develop logical characterizations in terms of expressive probabilistic modal mu-calculi and a novel real-valued modal logic. We prove that upper-expectation bisimilarity is a congruence for the wide family of process algebras specified following the probabilistic GSOS rule format.
△ Less
Submitted 2 October, 2013;
originally announced October 2013.
-
Łukasiewicz mu-Calculus
Authors:
Matteo Mio,
Alex Simpson
Abstract:
The paper explores properties of Łukasiewicz mu-calculus, a version of the quantitative/probabilistic modal mu-calculus containing both weak and strong conjunctions and disjunctions from Łukasiewicz (fuzzy) logic. We show that this logic encodes the well-known probabilistic temporal logic PCTL. And we give a model-checking algorithm for computing the rational denotational value of a formula at an…
▽ More
The paper explores properties of Łukasiewicz mu-calculus, a version of the quantitative/probabilistic modal mu-calculus containing both weak and strong conjunctions and disjunctions from Łukasiewicz (fuzzy) logic. We show that this logic encodes the well-known probabilistic temporal logic PCTL. And we give a model-checking algorithm for computing the rational denotational value of a formula at any state in a finite rational probabilistic nondeterministic transition system.
△ Less
Submitted 3 September, 2013;
originally announced September 2013.
-
Probabilistic modal μ-calculus with independent product
Authors:
Matteo Mio
Abstract:
The probabilistic modal μ-calculus is a fixed-point logic designed for expressing properties of probabilistic labeled transition systems (PLTS's). Two equivalent semantics have been studied for this logic, both assigning to each state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other…
▽ More
The probabilistic modal μ-calculus is a fixed-point logic designed for expressing properties of probabilistic labeled transition systems (PLTS's). Two equivalent semantics have been studied for this logic, both assigning to each state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other is a game semantics, specified in terms of two-player stochastic parity games. A shortcoming of the probabilistic modal μ-calculus is the lack of expressiveness required to encode other important temporal logics for PLTS's such as Probabilistic Computation Tree Logic (PCTL). To address this limitation we extend the logic with a new pair of operators: independent product and coproduct. The resulting logic, called probabilistic modal μ-calculus with independent product, can encode many properties of interest and subsumes the qualitative fragment of PCTL. The main contribution of this paper is the definition of an appropriate game semantics for this extended probabilistic μ-calculus. This relies on the definition of a new class of games which generalize standard two-player stochastic (parity) games by allowing a play to be split into concurrent subplays, each continuing their evolution independently. Our main technical result is the equivalence of the two semantics. The proof is carried out in ZFC set theory extended with Martin's Axiom at an uncountable cardinal.
△ Less
Submitted 26 November, 2012; v1 submitted 7 November, 2012;
originally announced November 2012.
-
On the equivalence of game and denotational semantics for the probabilistic mu-calculus
Authors:
Matteo Mio
Abstract:
The probabilistic (or quantitative) modal mu-calculus is a fixed-point logic de- signed for expressing properties of probabilistic labeled transition systems (PLTS). Two semantics have been studied for this logic, both assigning to every process state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotati…
▽ More
The probabilistic (or quantitative) modal mu-calculus is a fixed-point logic de- signed for expressing properties of probabilistic labeled transition systems (PLTS). Two semantics have been studied for this logic, both assigning to every process state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other is a game semantics, specified in terms of two-player stochastic games. The two semantics have been proved to coincide on all finite PLTS's, but the equivalence of the two semantics on arbitrary models has been open in literature. In this paper we prove that the equivalence indeed holds for arbitrary infinite models, and thus our result strengthens the fruitful connection between denotational and game semantics. Our proof adapts the unraveling or unfolding method, a general proof technique for proving result of parity games by induction on their complexity.
△ Less
Submitted 31 May, 2012; v1 submitted 1 May, 2012;
originally announced May 2012.
