Probabilistic Buchi automata are a natural generalization of PFA to infinite words, but have been studied in-depth only rather recently and many interesting questions are still open. PBA are known to accept, in genera...
详细信息
ISBN:
(纸本)9783030452315;9783030452308
Probabilistic Buchi automata are a natural generalization of PFA to infinite words, but have been studied in-depth only rather recently and many interesting questions are still open. PBA are known to accept, in general, a class of languages that goes beyond the regular languages. In this work we extend the known classes of restricted PBA which are still regular, strongly relying on notions concerning ambiguity in classical omega-automata. Furthermore, we investigate the expressivity of the not yet considered but natural class of weak PBA, and we also show that the regularity problem for weak PBA is undecidable.
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing pr...
详细信息
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing program logics are based on a low-level view of storage that is sensitive to the presence or absence of unreachable cells, and Reynolds has pointed out that the Hoare triples derivable in these logics are even incompatible with garbage collection. We present a study of a small language whose operational semantics includes a rule for reclaiming garbage. Our main results include an analysis of propositions that are garbage insensitive, and full abstraction results connecting partial and total correctness to two natural notions of observational equivalence between programs. (C) 2002 Elsevier science B.V. All rights reserved.
this book constitutes the proceedings of the 20thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2017, which took place in Uppsala, Sweden in April 2017, held as Part o...
详细信息
ISBN:
(数字)9783662544587
ISBN:
(纸本)9783662544570
this book constitutes the proceedings of the 20thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2017, which took place in Uppsala, Sweden in April 2017, held as Part of the European Joint conferences on theory and Practice of software, ETAPS 2017.
We prove that if a finite alphabet of actions contains at least two elements, then the equational theory for the process algebra BCCSP modulo any semantics no coarser than readiness equivalence and no finer than possi...
详细信息
ISBN:
(纸本)3540212981
We prove that if a finite alphabet of actions contains at least two elements, then the equational theory for the process algebra BCCSP modulo any semantics no coarser than readiness equivalence and no finer than possible worlds equivalence does not have a finite basis. this semantic range includes ready trace equivalence.
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples ...
详细信息
the compactness theorem and Godel's completeness theorem are perhaps the most important tools of mathematical logic for creating extensions of an existing model of a given theory. Unfortunately none of these theor...
详细信息
ISBN:
(纸本)9783540725039
the compactness theorem and Godel's completeness theorem are perhaps the most important tools of mathematical logic for creating extensions of an existing model of a given theory. Unfortunately none of these theorems hold if we restrict our attention to finite models. In this paper we give generalizations of these theorems which can be used to construct extensions of nonstandard versions of finite structures. therefore, although the structures are infinite, some finiteness properties will be true both for the original and the extended structures. these types of model extensions are closely related to questions in complexity theory.
Mean-payoff games play a central role in quantitative synthesis and verification. In a single-dimensional game a weight is assigned to every transition and the objective of the protagonist is to assure a non-negative ...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
Mean-payoff games play a central role in quantitative synthesis and verification. In a single-dimensional game a weight is assigned to every transition and the objective of the protagonist is to assure a non-negative limit-average weight. In the multidimensional setting, a weight vector is assigned to every transition and the objective of the protagonist is to satisfy a boolean condition over the limit-average weight of each dimension, e.g., LimAvg(xi) < 0 V LimAvg(x2) >= 0 A LimAvg(x3) >= 0. We recently proved that when one of the players is restricted to finite-memory strategies then the decidability of determining the winner is inter-reducible with Hilbert's Tenth problem over rationals (a fundamental long-standing open problem). In this work we consider arbitrary (infinite-memory) strategies for both players and show that the problem is undecidable.
this open access book constitutes the proceedings of the 24thinternationalconference on foundations of softwarescience and computational structures, FOSSACS 2021, which was held during March 27 until April 1, ...
详细信息
ISBN:
(数字)9783030719951
ISBN:
(纸本)9783030719944
this open access book constitutes the proceedings of the 24thinternationalconference on foundations of softwarescience and computational structures, FOSSACS 2021, which was held during March 27 until April 1, 2021, as part of the European Joint conferences on theory and Practice of software, ETAPS 2021. the conference was planned to take place in Luxembourg and changed to an online format due to the COVID-19 pandemic.
this open access book constitutes the proceedings of the 28thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2025, which took place in Hamilton, Canada, during May 2025...
详细信息
ISBN:
(数字)9783031908972
ISBN:
(纸本)9783031908965
this open access book constitutes the proceedings of the 28thinternationalconference on foundations of softwarescience and computationstructures, FOSSACS 2025, which took place in Hamilton, Canada, during May 2025, held as part of the international Joint conferences on theory and Practice of software, ETAPS 2025.
the 19 papers included in these proceedings were carefully reviewed and selected from 58 submissions. they focus on foundational research in softwarescience on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems.
We introduce a theory of weak bisimilarity for the pi-calculus with linear type structure [35] in which we abstract away not only tauactions but also non-tau actions which do not affect well-typed environments. this g...
详细信息
ISBN:
(纸本)354043366X
We introduce a theory of weak bisimilarity for the pi-calculus with linear type structure [35] in which we abstract away not only tauactions but also non-tau actions which do not affect well-typed environments. this gives an equivalence far larger than the standard bisimilarity while retaining semantic soundness. the congruency of the bisimilarity relies on a liveness property at linear channels ensured by typing. the theory is consistently extendible to settings which involve nontermination, nondeterminism and state. As an application we develop a behavioural theory of secrecy for the pi-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach in [20,23].
暂无评论