-
Laser Annealed SiO2/Si1-xGex Scaffolds for Nanoscaled Devices, Synergy of Experiment and Computation
Authors:
Damiano Ricciarelli,
Jonas Müller,
Guilhem Larrieu,
Ioannis Deretzis,
Gaetano Calogero,
Enrico Martello,
Giuseppe Fisicaro,
Jean-Michel Hartmann,
Sébastien Kerdilès,
Mathieu Opprecht,
Antonio Massimiliano Mio,
Richard Daubriac,
Fuccio Cristiano,
Antonino La Magna
Abstract:
Ultraviolet nanosecond laser annealing (UV-NLA) proves to be an important technique, particularly when tightly controlled heating and melting are necessary. In the realm of semiconductor technologies, the significance of nanosecond laser annealing (NLA) grows in tandem with the escalating intricacy of integration schemes in nano-scaled devices. Silicon-germanium alloys have been studied for decade…
▽ More
Ultraviolet nanosecond laser annealing (UV-NLA) proves to be an important technique, particularly when tightly controlled heating and melting are necessary. In the realm of semiconductor technologies, the significance of nanosecond laser annealing (NLA) grows in tandem with the escalating intricacy of integration schemes in nano-scaled devices. Silicon-germanium alloys have been studied for decades for their compatibility with silicon devices. Indeed, they enable the manipulation of properties like strain, carrier mobilities and bandgap. In this framework, they can for instance boost the performances of p-type MOSFETs but also enable near infra-red absorption and emission for applications in photo-detection and photonics. Laser melting on such type of layers, however results, up to now, in the development of extended defects and poor control over layer morphology and homogeneity. In our study, we investigate the laser melting of ~700 nm thick relaxed silicon-germanium samples coated with SiO2 nano-arrays, observing the resulting material to maintain an unaltered lattice. We found the geometrical parameters of the silicon oxide having an impact on the thermal budget samples see, influencing melt threshold, melt depth and germanium distribution.
△ Less
Submitted 6 May, 2024; v1 submitted 18 March, 2024;
originally announced March 2024.
-
Direct atomic layer deposition of ultra-thin $Al_{2}O_{3}$ and $HfO_{2}$ films on gold-supported monolayer $MoS_{2}$
Authors:
E. Schilirò,
S. E. Panasci,
A. M. Mio,
G. Nicotra,
S. Agnello,
B. Pecz,
G. Z. Radnoczi,
I. Deretzis,
A. La Magna,
F. Roccaforte,
R. Lo Nigro,
F. Giannazzo
Abstract:
In this paper, the atomic layer deposition (ALD) of ultra-thin films (<4 nm) of $Al_{2}O_{3}$ and $HfO_{2}$ on Au-supported monolayer (1L) $MoS_{2}$ is investigated, providing an insight on the nucleation mechanisms in the early stages of the ALD process. A preliminary multiscale characterization of large area 1L-$MoS_{2}$ exfoliated on sputter-grown Au/Ni films revealed an almost conformal…
▽ More
In this paper, the atomic layer deposition (ALD) of ultra-thin films (<4 nm) of $Al_{2}O_{3}$ and $HfO_{2}$ on Au-supported monolayer (1L) $MoS_{2}$ is investigated, providing an insight on the nucleation mechanisms in the early stages of the ALD process. A preliminary multiscale characterization of large area 1L-$MoS_{2}$ exfoliated on sputter-grown Au/Ni films revealed an almost conformal $MoS_{2}$ membrane with the Au topography and the occurrence of strain variations at the nanoscale. Ab-initio DFT calculations of $MoS_{2}$/Au(111) interface showed a significant influence of the Au substrate on the $MoS_{2}$ energy band structure, whereas small differences were accounted for the adsorption of the $H_{2}O$, TMA and TDMAHf precursors. This suggests a crucial role of nanoscale morphological effects, such as local curvature and strain of the $MoS_{2}$ membrane, in the enhanced physisorption of the precursors. Therefore, the nucleation and growth of $Al_{2}O_{3}$ and $HfO_{2}$ films onto 1L-$MoS_{2}$/Au was investigated, by monitoring the surface coverage as a function of the number (N) of ALD cycles, with N from 10 to 120. At low N values, a slower growth rate of the initially formed nuclei was observed for $HfO_{2}$, probably due to the bulky nature of the TDMAHf precursor as compared to TMA. On the other hand, the formation of continuous films was obtained in both cases for N>80 ALD cycles, corresponding to 3.6 nm $Al_{2}O_{3}$ and 3.1 nm $HfO_{2}$. Current map** by C-AFM showed, for the same applied bias, a uniform insulating behavior of $Al_{2}O_{3}$ and the occurrence of few localized breakdown spots in the case of $HfO_{2}$, associated to less compact films regions. Finally, an increase of the 1L-$MoS_{2}$ tensile strain was observed by Raman map** after encapsulation with both high-k films, accompanied by a reduction in the PL intensity.
△ Less
Submitted 13 May, 2023;
originally announced May 2023.
-
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 5 July, 2024; 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.
-
Simulation of the impact of people mobility, vaccination rate, and virus variants on the evolution of Covid-19 outbreak
Authors:
Corrado Spinella,
Antonio Massimiliano Mio
Abstract:
We have further extended our compartmental model describing the spread of the infection in Italy. The model is based on the assumption that the time evolution of all of the observable quantities (number of people still positive to the infection, hospitalized and fatalities cases, healed people, and total number of people that has contracted the infection) depend on average parameters, namely peopl…
▽ More
We have further extended our compartmental model describing the spread of the infection in Italy. The model is based on the assumption that the time evolution of all of the observable quantities (number of people still positive to the infection, hospitalized and fatalities cases, healed people, and total number of people that has contracted the infection) depend on average parameters, namely people diffusion coefficient, infection cross-section, and population density. The model provides precious information on the tight relationship between the variation of the reported infection cases and a well defined observable physical quantity: the average number of people that lie within the daily displacement area of any single person. The extension of the model now includes self-consistent evaluation of the reproduction index, effect of immunization due to vaccination, and potential impact of virus variants on the dynamical evolution of the outbreak. The model fits very well the epidemic data, and allows us to strictly relate the time evolution of the number of hospitalized case and fatalities to the change of people mobility, vaccination rate, and appearance of an initial concentration of people positives for new variants of the virus.
△ Less
Submitted 8 February, 2021; v1 submitted 4 February, 2021;
originally announced February 2021.
-
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.
-
Phenomenological description of spread of Covid-19 in Italy: people mobility as main factor controlling propagation of infection cases
Authors:
Corrado Spinella,
Antonio Massimiliano Mio
Abstract:
The spread of the coronavirus (COVID-19), starting in late 2019, has determined in Italy several interventions aimed to prevent saturation of the health system. We have examined the effects of such measures by proposing a mean-field model describing the spread of the infection based on a simple diffusion process where all the observable variables (number of people still positive to the infection,…
▽ More
The spread of the coronavirus (COVID-19), starting in late 2019, has determined in Italy several interventions aimed to prevent saturation of the health system. We have examined the effects of such measures by proposing a mean-field model describing the spread of the infection based on a simple diffusion process where all the observable variables (number of people still positive to the infection, hospitalized and fatalities cases, healed people, and total number of people that has contracted the infection) depend on average parameters, namely diffusion coefficient, infection cross-section, and population density. Although this model is less sophisticated than other models in the literature, it allows us to directly relate the trend of the epidemic statistical information (hospitalized cases, number of fatalities, number of infected people, etc.) to a well defined observable physical quantity: the average number of people that any individual meets per day. The model fits very well the epidemic data, and allows us to strictly relate the time evolution of the number of hospitalized case and fatalities of the outbreak to the change of people mobility, consequent to the implementation of progressive restrictions in Italy, running until the present days (November the 15th, 2020).
△ Less
Submitted 17 November, 2020; v1 submitted 16 November, 2020;
originally announced November 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.
-
Black Phosphorus/Palladium Nanohybrid: Unraveling the Nature of P-Pd Interaction and Application in Selective Hydrogenation
Authors:
Matteo Vanni,
Manuel Serrano-Ruiz,
Francesca Telesio,
Stefan Heun,
Martina Banchelli,
Paolo Matteini,
Antonio Massilimiliano Mio,
Giuseppe Nicotra,
Corrado Spinella,
Stefano Caporali,
Andrea Giaccherini,
Francesco d'Acapito,
Maria Caporali,
Maurizio Peruzzini
Abstract:
The burgeoning interest in 2D black phosphorus (bP) contributes to expand its applications in countless fields. In the present study, 2D bP is used as a support for homogeneously dispersed palladium nanoparticles directly grown on it by a wet chemical process. EELS-STEM analysis evidences a strong interaction between palladium and P atoms of bP nanosheets. A quantitative evaluation of this interac…
▽ More
The burgeoning interest in 2D black phosphorus (bP) contributes to expand its applications in countless fields. In the present study, 2D bP is used as a support for homogeneously dispersed palladium nanoparticles directly grown on it by a wet chemical process. EELS-STEM analysis evidences a strong interaction between palladium and P atoms of bP nanosheets. A quantitative evaluation of this interaction comes from XAS measurements that find out a very short Pd-P distance of 2.26 Å proving for the first time the existence of an unprecedented Pd-P coordination bond of covalent nature. Additionally, the average Pd-P coordination number of about 1.7 reveals that bP acts as a polydentate phosphine ligand towards the surface Pd atoms of the nanoparticles, thus preventing their agglomeration and inferring structural stability. These unique properties result in a superior performance in the catalytic hydrogenation of chloronitroarenes to chloroaniline, where a higher chemoselectivity in comparison to other heterogeneous catalyst based on palladium has been observed.
△ Less
Submitted 6 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.
