Showing 1–12 of 12 results for author: Terraf, P S

A classification of bisimilarities for general Markov decision processes

Authors: Martín Santiago Moroni, Pedro Sánchez Terraf

Abstract: We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity" from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci's notions of bisimilarity between two different processes to the case of… ▽ More We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity" from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci's notions of bisimilarity between two different processes to the case of nondeterministic LMP and generalize the game characterization of state bisimilarity by Clerc et al. for the latter. △ Less

Submitted 13 February, 2024; v1 submitted 17 January, 2024; originally announced January 2024.

Comments: 38 pages. v2: Reference to prior example due to D. Gburek and added acknowledgment

MSC Class: 68Q85 (Primary); 60Jxx; 03E15; 28A05 (Secondary) ACM Class: F.4.1

The formal verification of the ctm approach to forcing

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg

Abstract: We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$. Moreover, let $\mathcal{R}$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $Ω\subseteq\mathcal{R}$ and defined… ▽ More We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{CH}$. Moreover, let $\mathcal{R}$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $Ω\subseteq\mathcal{R}$ and defined $\mathcal{F}:\mathcal{R}\to\mathcal{R}$ such that for every $Φ\subseteq\mathcal{R}$ and $M$-generic $G$, $M\models \mathit{ZC} \cup \mathcal{F}\text{``}Φ\cup Ω$ implies $M[G]\models \mathit{ZC} \cup Φ\cup \{ \neg \mathit{CH} \}$, where $\mathit{ZC}$ is Zermelo set theory with Choice. To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others. △ Less

Submitted 14 December, 2023; v1 submitted 27 October, 2022; originally announced October 2022.

Comments: 20pp + 14pp in bibliography & appendices, 2 tables. v2: Added details to Delta System Lemma appendix, updated acknowledgments

MSC Class: 68V20 (Primary) 03E35; 03E30 (Secondary) ACM Class: F.4.1; I.2.3

The Zhou Ordinal of Labelled Markov Processes over Separable Spaces

Authors: Martín Santiago Moroni, Pedro Sánchez Terraf

Abstract: There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed poi… ▽ More There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator $\mathcal{O}$, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the "Zhou ordinal" of $\mathbb{S}$, $\mathfrak{Z}(\mathbb{S})$. When $\mathfrak{Z}(\mathbb{S})=0$, $\mathbb{S}$ satisfies the Hennessy-Milner property. The second author proved the existence of an LMP $\mathbb{S}$ with $\mathfrak{Z}(\mathbb{S}) \geq 1$ and Zhou showed that there are LMPs having an infinite Zhou ordinal. In this paper we show that there are LMPs $\mathbb{S}$ over separable metrizable spaces having arbitrary large countable $\mathfrak{Z}(\mathbb{S})$ and that it is consistent with the axioms of $\mathit{ZFC}$ that there is such a process with an uncountable Zhou ordinal. △ Less

Submitted 22 December, 2022; v1 submitted 7 May, 2020; originally announced May 2020.

Comments: v1: 19 pages. v2: role of the logic on Introduction, relation with previous constructions and 1 figure. Many minor corrections. v3: 20 pages. First item in former Lemma 30 was incorrect, but all the main results are still correct. Accepted at Review of Symbolic Logic. We are very grateful for the referee's useful suggestions and detailed reading

MSC Class: 68Q85 (Primary); 60Jxx; 03E15; 28A05 (Secondary) ACM Class: F.4.1

Formalization of Forcing in Isabelle/ZF

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Abstract: We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library. We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library. △ Less

Submitted 18 April, 2020; v1 submitted 27 January, 2020; originally announced January 2020.

Comments: 15 pages. Accepted at the 10th International Joint Conference on Automated Reasoning (IJCAR 2020). v2: Added expanded section on related work

MSC Class: 03B35 (Primary) 03E40; 03B70; 68T15 (Secondary) ACM Class: F.4.1

Mechanization of Separation in Generic Extensions

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Abstract: We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these… ▽ More We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson's library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened hypotheses in his development of relativization and absoluteness. △ Less

Submitted 10 January, 2019; originally announced January 2019.

Comments: 23 pages, 1 figure

MSC Class: 03B35 (Primary) 03E40; 03B70; 68T15 (Secondary) ACM Class: F.4.1

First steps towards a formalization of Forcing

Authors: Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Abstract: We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski… ▽ More We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does. We also prove $M[G]$ is transitive. △ Less

Submitted 27 November, 2018; v1 submitted 13 July, 2018; originally announced July 2018.

Comments: 18 pages. Isabelle proofs can be found among the source files of this submission. v2: Added discussion of related work and of details of implementation. Proof that G belongs to M[G] and that the latter is transitive

MSC Class: 03B35 (Primary) 03E40; 03B70; 68T15 (Secondary) ACM Class: F.4.1

Semipullbacks of labelled Markov processes

Authors: Jan Pachl, Pedro Sánchez Terraf

Abstract: A labelled Markov process (LMP) consists of a measurable space $S$ together with an indexed family of Markov kernels from $S$ to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problems in the area is to define and decide whether two LMP $S$ and $S'$ "behave the same". There are two natural categorical definitions of sameness of beh… ▽ More A labelled Markov process (LMP) consists of a measurable space $S$ together with an indexed family of Markov kernels from $S$ to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problems in the area is to define and decide whether two LMP $S$ and $S'$ "behave the same". There are two natural categorical definitions of sameness of behavior: $S$ and $S'$ are bisimilar if there exist an LMP $ T$ and measure preserving maps forming a diagram of the shape $ S\leftarrow T \rightarrow{S'}$; and they are behaviorally equivalent if there exist some $ U$ and maps forming a dual diagram $ S\rightarrow U \leftarrow{S'}$. These two notions differ for general measurable spaces but Doberkat (extending a result by Edalat) proved that they coincide for analytic Borel spaces, showing that from every diagram $S\rightarrow U \leftarrow{S'}$ one can obtain a bisimilarity diagram as above. Moreover, the resulting square of measure preserving maps is commutative (a semipullback). In this paper, we extend the previous result to measurable spaces $S$ isomorphic to a universally measurable subset of a Polish space with the trace of the Borel $σ$-algebra, using a version of Strassen's theorem on common extensions of finitely additive measures. △ Less

Submitted 12 April, 2021; v1 submitted 8 June, 2017; originally announced June 2017.

MSC Class: 28A35; 28A60; 68Q85 ACM Class: F.4.1; F.1.2

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 2 (April 14, 2021) lmcs:5886

The Lattice of Congruences of a Finite Line Frame

Authors: Carlos Areces, Miguel Campercholi, Daniel Penazzi, Pedro Sánchez Terraf

Abstract: Let $\mathbf{F}=\left\langle F,R\right\rangle $ be a finite Kripke frame. A congruence of $\mathbf{F}$ is a bisimulation of $\mathbf{F}$ that is also an equivalence relation on F. The set of all congruences of $\mathbf{F}$ is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that $\mathbf{F}$ is a finite line frame. We give concrete descriptions of the… ▽ More Let $\mathbf{F}=\left\langle F,R\right\rangle $ be a finite Kripke frame. A congruence of $\mathbf{F}$ is a bisimulation of $\mathbf{F}$ that is also an equivalence relation on F. The set of all congruences of $\mathbf{F}$ is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that $\mathbf{F}$ is a finite line frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence $ρ$, the interval $[\mathrm{Id_{F},ρ]}$ embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute. △ Less

Submitted 10 April, 2017; v1 submitted 7 April, 2015; originally announced April 2015.

Comments: 31 pages, 11 figures. Expanded intro, conclusions rewritten. New, less geometrical, proofs of Lemma 19 and (former) Lemma 34

MSC Class: 03B45 (Primary); 06B10; 06E25; 03B70 (Secondary) ACM Class: F.4.1; F.1.2

Stochastic Nondeterminism and Effectivity Functions

Authors: Ernst-Erich Doberkat, Pedro Sánchez Terraf

Abstract: This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernel… ▽ More This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernels used for defining two different models: Nondeterministic labelled Markov processes and stochastic game models, respectively. We show that an effectivity function that maps into principal filters is given by an image-countable nondeterministic kernel, and that image-finite kernels give rise to effectivity functions. We define state bisimilarity for the latter, considering its connection to morphisms. We provide a logical characterization of bisimilarity in the finitary case. A generalization of congruences (event bisimulations) to effectivity functions and its relation to the categorical presentation of bisimulation are also studied. △ Less

Submitted 5 July, 2015; v1 submitted 28 May, 2014; originally announced May 2014.

Comments: Minor changes in the text, correction of typos; new and extended abstract; added an acknowledgement (paper accepted by J. Logic Comput.)

Report number: SWT-Memo 200 MSC Class: 03B70; 03E15; 28A05 ACM Class: F.4.1; F.1.2

Bisimilarity is not Borel

Authors: Pedro Sánchez Terraf

Abstract: We prove that the relation of bisimilarity between countable labelled transition systems is $Σ_1^1$-complete (hence not Borel), by reducing the set of non-wellorders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and nondeterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on… ▽ More We prove that the relation of bisimilarity between countable labelled transition systems is $Σ_1^1$-complete (hence not Borel), by reducing the set of non-wellorders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and nondeterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on the unique structure theorem for analytic spaces) require a countable logic whose formulas have measurable semantics. Our reduction shows that such a logic does not exist in the case of image-infinite processes. △ Less

Submitted 21 February, 2014; v1 submitted 5 November, 2012; originally announced November 2012.

Comments: 20 pages, 1 figure; proof of Sigma_1^1 completeness added with extended comments. I acknowledge careful reading by the referees. Major changes in Introduction, Conclusion, and motivation for NLMP. Proof for Lemma 22 added, simpler proofs for Lemma 17 and Theorem 30. Added references. Part of this work was presented at Dagstuhl Seminar 12411 on Coalgebraic Logics

MSC Class: 03B70; 03E15; 28A05 ACM Class: F.4.1; F.1.2

Bisimulations for Nondeterministic Labeled Markov Processes

Authors: Pedro D'Argenio, Pedro Sánchez Terraf, Nicolás Wolovick

Abstract: We extend the theory of labeled Markov processes with internal nondeterminism, a fundamental concept for the further development of a process theory with abstraction on nondeterministic continuous probabilistic systems. We define nondeterministic labeled Markov processes (NLMP) and provide three definition of bisimulations: a bisimulation following a traditional characterization, a state based b… ▽ More We extend the theory of labeled Markov processes with internal nondeterminism, a fundamental concept for the further development of a process theory with abstraction on nondeterministic continuous probabilistic systems. We define nondeterministic labeled Markov processes (NLMP) and provide three definition of bisimulations: a bisimulation following a traditional characterization, a state based bisimulation tailored to our "measurable" non-determinism, and an event based bisimulation. We show the relation between them, including that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy-Milner logic that characterizes event bisimulation and that is sound w.r.t. the other bisimulations for arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable $\lor$. We then introduce a finitary sublogic that characterize all bisimulations for image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all notions of bisimulation we deal with turn out to be equal. Finally, we show that all notions of bisimulations are different in the general case. The counterexamples that separate them turn to be non-probabilistic NLMP. △ Less

Submitted 15 November, 2010; originally announced November 2010.

MSC Class: 60Jxx ACM Class: G.3; F.4.1

Unprovability of the Logical Characterization of Bisimulation

Authors: Pedro Sánchez Terraf

Abstract: We quickly review labelled Markov processes (LMP) and provide a counterexample showing that in general measurable spaces, event bisimilarity and state bisimilarity differ in LMP. This shows that the logic in Desharnais [*] does not characterize state bisimulation in non-analytic measurable spaces. Furthermore we show that, under current foundations of Mathematics, such logical characterization i… ▽ More We quickly review labelled Markov processes (LMP) and provide a counterexample showing that in general measurable spaces, event bisimilarity and state bisimilarity differ in LMP. This shows that the logic in Desharnais [*] does not characterize state bisimulation in non-analytic measurable spaces. Furthermore we show that, under current foundations of Mathematics, such logical characterization is unprovable for spaces that are projections of a coanalytic set. Underlying this construction there is a proof that stationary Markov processes over general measurable spaces do not have semi-pullbacks. ([*] J. Desharnais, Labelled Markov Processes. School of Computer Science. McGill University, Montréal (1999)) △ Less

Submitted 10 December, 2010; v1 submitted 27 May, 2010; originally announced May 2010.

Comments: Extended introduction and comments; extra section on semi-pullbacks; 11 pages Some background details added; extra example on the non-locality of state bisimilarity; 14 pages

MSC Class: 03E15; 28A05; 60Jxx ACM Class: G.3; F.4.1