ABSTRACT. Link to abstract

ABSTRACT. In a discussion on the computational complexity of "parameterized" NL (nondeterministic logarithmic-space complexity class), Syntactic NL or succinctly SNL was first introduced in 2017 as a "syntactically"-defined natural subclass of NL using a restricted form of second-order logic in close connection to the so-called linear space hypothesis. We further explore various properties of this complexity class SNL. In particular, we consider the expressibility of "complementary" problems of SNL problems. As variants of SNL, we also study an optimization version of SNL, called MAXSNL, and its subclass, called MAX\tauSNL.

ABSTRACT. The rule of orthomodularity is important, for example due to its foundational role in quantum logic. However, orthomodularity is a restriction that is not always suitable. For example, orthomodularity is not fulfilled by certain geometric structures such as the lattice of closed convex cones, which is different from the lattice considered in quantum logic, namely that of closed subspaces of a Hilbert space. Thus, the question arises whether the rule of orthomodularity can be relaxed such that the relaxed rule is still stronger than the ortholattice rule and such that each orthomodular lattice fulfills also the relaxed rule. Therefore, we present two rules of partial orthomodularity of different strength, (pOM) and (pOMex), which keep some of the advantages of the rule of orthomodularity but are relaxations of it. We show the validity and usefulness of these rules by proving a subalgebra theorem for (pOM), by showing that an algebraic representation theorem for orthomodularity can be relaxed as to be based on the rules of partial orthomodularity and by proving a connection to Johansson’s minimal rule.

ABSTRACT. The combination of probability and nondeterminism in state-based systems is a notoriously challenging problem, mainly due to the known lack of a Beck distributive law between the powerset and probability monads. In this talk I will introduce a version of probabilistic Kleene algebra and a corresponding class of automata with nondeterminism formalized by multisets instead of powersets, based on the recently established Beck distributive law of probability over multisets by Jacobs. I will describe the operational and denotational semantics of automata and expressions and give a Kleene theorem in both directions.

(joint work with Shawn Ong and Stephanie Ma)

ABSTRACT. Separation logic (SL) is extensively employed in verification to analyze programs that manipulate dynamically allocated memory. The entailment problem, when dealing with inductively defined predicates and/or data constraints, is undecidable for SL formulas. Our focus is on addressing a specific fragment of this issue, wherein the consequent is restricted to clauses of some particular form, devoid of inductively defined predicates. We present an algorithm designed to determine the validity of such entailments and demonstrate that the problem is decidable and EXPTIME complete under some conditions on the data theory. This algorithm serves the purpose of verifying that the data structures outlined by a given SL formula (the antecedent) adhere to certain shape constraints expressed by the consequent.

ABSTRACT. In the vein of recent work that provides non-normal modal interpretations of various topological operators, this paper proposes a modal logic for a spatial isolation operator. Focussing initially on neighborhood systems, we prove several characterization results, demonstrating the adequacy of the interpretation and highlighting certain semantic insensitivities that result from the relative expressive weakness of the isolation operator. We then transition to the topological setting, proving a result for discrete spaces.