[1]

Semipullbacks of labelled Markov processes.
Logical Methods in Computer Science, 17 (2) (Apr.
2021).
arXiv:1706.02801.
Joint work with J. Pachl.
[ bib 
DOI 
arXiv 
http ]
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← T →S'; and they
are behaviorally equivalent
if there exist some U and maps forming a dual diagram
S→ U ←S'.
These two notions differ for general measurable spaces but Edalat
proved that they coincide for analytic Borel spaces, showing that
from every
diagram S→ U ←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 Edalat's 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.

[2]

Every minimal dual discriminator variety is minimal as a quasivariety.
Algebra universalis, 82 (2): 36 (Apr 2021).
Joint work with X. Caicedo, M. Campercholi, K. A. Kearnes,
Á. Szendrei, and D. Vaggione.
[ bib 
DOI 
http ]
Let † denote the following property of a variety V: Every subquasivariety of V is a variety. In this paper, we prove that every idempotent dual discriminator variety has property † . Property † need not hold for nonidempotent dual discriminator varieties, but † does hold for minimal nonidempotent dual discriminator varieties. Combining the results for the idempotent and nonidempotent cases, we obtain that every minimal dual discriminator variety is minimal as a quasivariety

[3]

The Zhou ordinal of labelled Markov processes over separable spaces.
arXiv eprints (May 2020).
arXiv:2005.03630.
Accepted for publication at the Review of Symbolic Logic.
Joint work with M. S. Moroni.
[ bib 
arXiv ]
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 O, and thus introduced an
ordinal measure of the discrepancy between it and event bisimilarity. We call
this ordinal the "Zhou ordinal" of S, Z(S).
When Z(S)=0, S satisfies the HennessyMilner
property. The second author proved the existence of an LMP S with
Z(S) ≥1 and Zhou showed that there are LMPs having an
infinite Zhou ordinal. In this paper we show that there are LMPs S
over separable metrizable spaces having arbitrary large countable
Z(S) and that it is consistent with the axioms of
ZFC that there is such a process with an uncountable Zhou ordinal.

[4]

Mechanization of Separation in Generic Extensions.
arXiv eprints, 1901.03313 (Jan. 2019).
arXiv:1901.03313.
Joint work with E. Gunther and M. Pagano.
[ bib 
arXiv ]
We mechanize, in the proof assistant Isabelle, a proof of the axiomscheme 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 wellfounded relations, and sharpened hypotheses in his development of relativization and absoluteness.

[5]

The Lattice of Congruences of a Finite Linear Frame.
Journal of Logic and Computation, 27: 2653–2688
(Apr. 2017).
1504.01789.
Joint work with C. Areces, M. Campercholi, and D. Penazzi.
[ bib 
DOI 
arXiv ]
Let F=⟨F,R⟩ be a finite Kripke frame. A
congruence of F is a bisimulation of F that is also an
equivalence relation on F. The set of all congruences of F is a
lattice under the inclusion ordering. In this article we investigate this
lattice in the case that F is a finite linear 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 [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.

[6]

Bisimilarity is not Borel.
Mathematical Structures in Computer Science, 27 (7):
1265–1284 (10 2017).
[ bib 
DOI 
http ]
We prove that the relation of bisimilarity between countable labelled transition systems is Σ_{1}^{1}complete (hence not Borel), by reducing the set of nonwellorders 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 imageinfinite processes.

[7]

Stochastic nondeterminism and effectivity functions.
Journal of Logic and Computation (2015).
1405.7141.
Joint work with E.E. Doberkat.
[ bib 
DOI 
arXiv ]
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 upperclosed 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 imagecountable nondeterministic kernel, and that imagefinite 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.

[8]

Bisimulations for nondeterministic labelled Markov processes.
Mathematical Structures in Comp. Sci., 22 (1): 43–68
(Feb. 2012).
Joint work with P. R. D'Argenio and N. Wolovick.
[ bib 
DOI 
http ]
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” nondeterminism, 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 HennessyMilner 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
.
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
nonprobabilistic NLMP.

[9]

Factor congruences in semilattices.
Revista de la Unión Matemática Argentina,
52 (1): 1–10 (2011).
0809.3822.
[ bib 
arXiv 
.pdf ]
We characterize factor congruences in semilattices by using generalized notions of order ideal and of direct sum of ideals. When the semilattice has a minimum
(maximum) element, these generalized ideals turn into ordinary (dual) ideals.

[10]

Boolean factor congruences and property (*).
Int. J. Algebra Comput., 21 (6): 931–950 (2011).
[ bib 
DOI ]
Summary: A variety V has Boolean factor congruences (BFC) if
the set of factor congruences of any algebra in V is a distributive
sublattice of its congruence lattice; this property holds in rings with unit
and in every variety which has a semilattice operation. BFC has a prominent
role in the study of uniqueness of direct product representations of
algebras, since it is a strengthening of the refinement property.
We
provide an explicit Mal'tsev condition for BFC. With the aid of this
condition, it is shown that BFC is equivalent to a variant of the
definability property (*), an open problem in R. Willard's work [J.
Algebra 132, No. 1, 130–153 (1990; Zbl 0737.08006)].

[11]

Unprovability of the logical characterization of bisimulation.
Information and Computation, 209 (7): 1048–1056
(2011).
[ bib 
DOI 
http ]
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 the work by Desharnais does not
characterize state bisimulation in nonanalytic 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 semipullbacks.

[12]

Existentially definable factor congruences.
Acta Scientiarum Mathematicarum (Szeged), 76 (1–2):
49–53 (2010).
0906.4722.
[ bib 
arXiv 
http ]
A variety V has definable factor congruences if and only if
factor congruences can be defined by a firstorder formula Φ having
central elements as parameters. We prove that if Φ
can be chosen to be existential, factor congruences in every
algebra of V are compact.

[13]

Varieties with definable factor congruences.
Trans. Amer. Math. Soc., 361: 5061–5088 (2009).
Joint work with D. Vaggione.
[ bib 
DOI ]
We study direct product representations of algebras in
varieties. We collect several
conditions expressing that these representations are definable
in a firstorderlogic sense, among them the concept of Definable
Factor Congruences (DFC). The main results are that DFC is a Mal'cev
property and that it is equivalent to all other conditions
formulated; in particular we prove that V has DFC if and only if
V has 0⃗ & 1⃗ and Boolean Factor Congruences. We also obtain an explicit
first order definition Φ of the kernel of the canonical projections via the terms
associated to the Mal'cev condition for DFC, in such a manner it is preserved
by taking direct products and direct factors. The main tool is the use
of central elements, which are a generalization of
both central idempotent elements in rings with identity and neutral
complemented elements in a bounded lattice.

[14]

Directly indecomposables in semidegenerate varieties of connected pogroupoids.
Order, 25 (4): 377–386 (2008).
[ bib 
DOI ]
We study varieties with a termdefinable poset structure, pogroupoids. It is known
that connected posets have the strict refinement property
(SRP). In a previous work by Vaggione and the author it is proved that
semidegenerate varieties with the SRP have definable factor congruences
and if the similarity type is finite, directly indecomposables are
axiomatizable by a set of firstorder sentences. We obtain such a set
for semidegenerate varieties of connected pogroupoids
and show its quantifier complexity is bounded in general.

[15]

Compact factor congruences imply Boolean factor congruences.
Algebra univers., 51: 207–213 (2004).
Joint work with D. Vaggione.
[ bib 
DOI ]
We prove that any variety V in which every factor congruence is compact has Boolean factor congruences, i.e., for all A in V the set of factor congruences of A is a distributive sublattice of the congruence lattice of A.
