Logic in Computer Science
See recent articles
- [1] arXiv:2407.13339 [pdf, other]
-
Title: On the complexity of Maslov's class $\overline{\text{K}}$Comments: This is an extended version of the LICS'24 paperSubjects: Logic in Computer Science (cs.LO)
Maslov's class $\overline{\text{K}}$ is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that $\overline{\text{K}}$ has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments studied in the literature, and propose a new decidable extension of the uniform one-dimensional fragment (without equality). Our approach involves a use of satisfiability games tailored to $\overline{\text{K}}$ and a novel application of paradoxical tournament graphs.
New submissions for Friday, 19 July 2024 (showing 1 of 1 entries )
- [2] arXiv:2407.12840 (cross-list from math.CT) [pdf, other]
-
Title: Categorical Foundations of Formalized Condensed MathematicsDagur Asgeirsson, Riccardo Brasca (IMJ-PRG (UMR\_7586)), Nikolas Kuhn (UiO), Filippo Alberto Edoardo Nuccio Mortarino Majno Di Capriglio (ICJ, UJM, CTN), Adam TopazSubjects: Category Theory (math.CT); Logic in Computer Science (cs.LO)
Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept of a topological space by that of a condensed set, which can be defined as a sheaf for the coherent topology on a certain category of compact Hausdorff spaces. In this case, the sheaf condition has a fairly simple explicit description, which arises from studying the relationship between the coherent, regular and extensive topologies. In this paper, we establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces. Along the way, we also provide a characterizations of sheaves and covering sieves for these categories. All results in this paper have been fully formalized in the Lean proof assistant.
- [3] arXiv:2407.13406 (cross-list from cs.FL) [pdf, html, other]
-
Title: Quasi-stratified Order Semantics of ConcurrencyComments: 18 pages, 6 figuresSubjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
In the development of operational semantics of concurrent systems, a key decision concerns the adoption of a suitable notion of execution model, which basically amounts to choosing a class of partial orders according to which events are arranged along the execution line. Typical kinds of such partial orders are the total, stratified and interval orders. In this paper, we introduce quasi-stratified orders - positioned in-between the stratified and interval orders - which are tailored for transaction-like or hierarchical concurrent executions.
Dealing directly with the vast number of executions of concurrent system is far from being practical. It was realised long time ago that it can be much more effective to consider behaviours at a more abstract level of behavioural specifications (often based on intrinsic relationships between events such as those represented by causal partial orders), each such specification - typically, a relational structure - encompassing a (large) number of executions.
In this paper, we introduce and investigate suitable specifications for behaviours represented by quasi-stratified orders. The proposed model of quasi-stratified relational structures is based on two relationships between events - the 'before' and 'not later' relationships - which can be used to express and analyse causality, independence, and simultaneity between events.
Cross submissions for Friday, 19 July 2024 (showing 2 of 2 entries )
- [4] arXiv:2312.14587 (replaced) [pdf, html, other]
-
Title: Measuring well quasi-ordered finitary powersetsComments: 27 pagesSubjects: Logic in Computer Science (cs.LO); Discrete Mathematics (cs.DM)
The complexity of a well-quasi-order (wqo) can be measured through three ordinal invariants: the width as a measure of antichains, height as a measure of chains, and maximal order type as a measure of bad sequences.
We study these ordinal invariants for the finitary powerset, i.e., the collection Pf(A) of finite subsets of a wqo A ordered with the Hoare embedding relation. We show that the invariants of Pf(A) cannot be expressed as a function of the invariants of A, and provide tight upper and lower bounds for them.
We then focus on a family of well-behaved wqos, for which these invariants can be computed compositionally, using a newly defined ordinal invariant called the approximate maximal order type. This family is built from multiplicatively indecomposable ordinals, using classical operations such as disjoint unions, products, finite words, finite multisets, and the finitary powerset construction. - [5] arXiv:2405.13697 (replaced) [pdf, html, other]
-
Title: The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrumComments: 66 pages, 1 figureSubjects: Logic in Computer Science (cs.LO)
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking.
This paper studies the complexity of determining whether a formula is characteristic for some finite, loop-free process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek's branching-time spectrum. Since characteristic formulae in each of those logics are exactly the consistent and prime ones, it presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard.
Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations. - [6] arXiv:2407.06391 (replaced) [pdf, other]
-
Title: Around Classical and Intuitionistic Linear ProcessesComments: Full version, 19 pages + appendicesSubjects: Logic in Computer Science (cs.LO)
Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classic versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent (2018), we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey (2017). Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.
- [7] arXiv:2407.06952 (replaced) [pdf, html, other]
-
Title: Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$Comments: Based on Ch. 3 and Sec. 5.1 of the author's PhD thesis (arXiv:2301.12405). v3: Updated AcknowledgementsSubjects: Logic in Computer Science (cs.LO); Logic (math.LO)
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in a variety of fields, such as programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that iterative constructions of dcpos may result in a need for ever-increasing universes and are predicatively impossible. We show, through a careful tracking of type universe parameters, that such constructions can be carried out in a predicative setting. In particular, we give a predicative reconstruction of Scott's $D_\infty$ model of the untyped $\lambda$-calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.
- [8] arXiv:2407.06956 (replaced) [pdf, html, other]
-
Title: Domain theory in univalent foundations II: Continuous and algebraic domainsComments: Based on Ch. 4 of the author's PhD thesis (arXiv:2301.12405). v3: Updated AcknowledgementsSubjects: Logic in Computer Science (cs.LO); Logic (math.LO)
We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. To deal with size issues and give a predicatively suitable definition of continuity of a dcpo, we follow Johnstone and Joyal's work on continuous categories. Adhering to the univalent perspective, we explicitly distinguish between data and property. To ensure that being continuous is a property of a dcpo, we turn to the propositional truncation, although we explain that some care is needed to avoid needing the axiom of choice. We also adapt the notion of a domain-theoretic basis to the predicative setting by imposing suitable smallness conditions, analogous to the categorical concept of an accessible category. All our running examples of continuous dcpos are then actually examples of dcpos with small bases which we show to be well behaved predicatively. In particular, such dcpos are exactly those presented by small ideals. As an application of the theory, we show that Scott's $D_\infty$ model of the untyped $\lambda$-calculus is an example of an algebraic dcpo with a small basis. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.
- [9] arXiv:2407.08688 (replaced) [pdf, html, other]
-
Title: A Unifying Categorical View of Nondeterministic Iteration and TestsComments: Full version of the CONCUR 2024 paperSubjects: Logic in Computer Science (cs.LO)
We study Kleene iteration in the categorical context. A celebrated completeness result by Kozen introduced Kleene algebra (with tests) as a ubiquitous tool for lightweight reasoning about program equivalence, and yet, numerous variants of it came along afterwards to answer the demand for more refined flavors of semantics, such as stateful, concurrent, exceptional, hybrid, branching time, etc. We detach Kleene iteration from Kleene algebra and analyze it from the categorical perspective. The notion, we arrive at is that of Kleene-iteration category (with coproducts and tests), which we show to be general and robust in the sense of compatibility with programming language features, such as exceptions, store, concurrent behavior, etc. We attest the proposed notion w.r.t. various yardsticks, most importantly, by characterizing the free model as a certain category of (nondeterministic) rational trees.
- [10] arXiv:2407.12677 (replaced) [pdf, html, other]
-
Title: Tree algebras and bisimulation-invariant MSO on finite graphsSubjects: Logic in Computer Science (cs.LO)
We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognized by finitary tree algebras whose sorts zero and one are finite are the regular ones, ie. the ones expressible in mu-calculus. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees since twenty years.