arXiv subjects

Harsh Beohar

Publications and source records attributed to Harsh Beohar.

At least 19 recordsLinked to original sources

arXiv2026

Languages and Recognition in a Category with Factorisation

Language recognition by homomorphisms is a central construction of algebraic language theory. Initially studied for monoids and semigroups, it has subsequently been expanded to other algebraic structures. Our new categorical account is based on fibrations, which have already seen other applications in automata theory. Languages and surjective homomorphisms give indeed rise to two fibrations, and the notion of language recognition is stable under reindexing. We develop this framework in a category with a factorisation system and address two main technical questions in the fibrational setting. First, we provide sufficient conditions under which languages have syntactic quotients (which is a generalisation of syntactic congruences) and we show how such quotients can be described in some concrete cases using a result by Slomi\'nski. Second, we introduce sufficient conditions under which (regular) languages are closed under certain J-limits and J-colimits.

cs.FL↗

arXiv2026

A coalgebraic higher-order modal fixed-point logic

We introduce a coalgebraic extension of the higher-order modal fixed-point logic (HFL) which subsumes both HFL and its probabilistic extension. We show that the emptiness problem for non-deterministic finite automata as well as the value-1 problem for probabilistic automata reduce to model-checking problems for this coalgebraic formulation of HFL.

cs.LO↗

arXiv2026

Tree Automata Acceptance up to Measurable Defect

Automata acceptance can, in several situations of interest, be captured game-theoretically via acceptance games. The existence of a winning strategy for Verifier then captures the existence of a winning run-tree of a given automaton over a model. However, such acceptance is rigid, in that it does not allow a measurable defect budget, which can be a challenge in software verification. In this paper, we draw inspiration from how bisimulation distance can be defined as an extension of bisimilarity to define epsilon-acceptance games. Our main theorem shows that a tree T is epsilon-accepted iff there is a tree T' that is accepted in the traditional (rigid) sense and the bisimulation distance of T' and T is at most epsilon. Our work also suggests a strong connection with measure theory, of which we give a preliminary exploration via appropriate examples. Our framework is defined over binary trees with leaves and infinite branches, and strictly contains the case in which binary nodes are seen as probabilistic choice and the defect measures the probability of the set of rejected branches.

cs.LO↗

arXiv2025

Expressivity of bisimulation pseudometrics over analytic state spaces

A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of measurable spaces. Note that analytic spaces were already studied in the literature on labelled Markov processes and bisimulation relations. Our results are twofold. First, we define bisimulation pseudometrics over such coalgebras using the framework of fibrations. Second, we develop a quantitative modal logic for such coalgebras and prove a quantitative form of Hennessy-Milner theorem in this new setting stating that the bisimulation pseudometric corresponds to the logical distance induced by modal formulae.

cs.LO↗

arXiv2025

Constructing Witnesses for Lower Bounds on Behavioural Distances

Behavioural distances provide a robust alternative to notions of equivalence such as bisimilarity in the context of probabilistic transition systems. They can be defined as least fixed points, whose universal property allows us to exhibit upper bounds on the distance between states, showing them to be at most some distance apart. In this paper, we instead consider the problem of bounding distances from below, showing states to be at least some distance apart. Contrary to upper bounds, it is possible to reason about lower bounds inductively. We exploit this by giving an inductive derivation system for lower bounds on an existing definition of behavioural distance for labelled Markov chains. This is inspired by recent work on apartness as an inductive counterpart to bisimilarity. Proofs in our system will be shown to closely match the behavioural distance by soundness and (approximate) completeness results. We further provide a constructive correspondence between our derivation system and formulas in a modal logic with quantitative semantics. This logic was used in recent work of Rady and van Breugel to construct evidence for lower bounds on behavioural distances. Our constructions provide smaller witnessing formulas in many examples.

cs.LO↗

arXiv2024

On Kleisli liftings and decorated trace semantics

It is well known that Kleisli categories provide a natural language to model side effects. For instance, in the theory of coalgebras, behavioural equivalence coincides with language equivalence (instead of bisimilarity) when nondeterministic automata are modelled as coalgebras living in the Kleisli category of the powerset monad. In this paper, our aim is to establish decorated trace semantics based on language and ready equivalences for conditional transition systems (CTSs) with/without upgrades. To this end, we model CTSs as coalgebras living in the Kleisli category of a relative monad. Our results are twofold. First, we reduce the problem of defining a Kleisli lifting for the machine endofunctor in the context of a relative monad to the classical notion of Kleisli lifting. Second, we provide a recipe based on indexed categories to construct a Kleisli lifting for general endofunctors.

cs.LO↗

arXiv2024

Relating Apartness and Branching Bisimulation Games

Geuvers and Jacobs (LMCS 2021) formulated the notion of apartness relation on state-based systems modelled as coalgebras. In this context apartness is formally dual to bisimilarity, and gives an explicit proof system for showing that certain states are not bisimilar. In the current paper, we relate apartness to another classical element of the theory of behavioural equivalences: that of turn-based two-player games. Studying both strong and branching bisimilarity, we show that winning configurations for the Spoiler player correspond to apartness proofs, for transition systems that are image-finite (in the case of strong bisimilarity) and finite (in the case of branching bisimilarity).

cs.LO↗

arXiv2024

Proving Behavioural Apartness

Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems. We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples.

cs.LO↗

arXiv2023

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).

cs.LO↗

arXiv2023

Graded Semantics and Graded Logics for Eilenberg-Moore Coalgebras

Coalgebra, as the abstract study of state-based systems, comes naturally equipped with a notion of behavioural equivalence that identifies states exhibiting the same behaviour. In many cases, however, this equivalence is finer than the intended semantics. Particularly in automata theory, behavioural equivalence of nondeterministic automata is essentially bisimilarity, and thus does not coincide with language equivalence. Language equivalence can be captured as behavioural equivalence on the determinization, which is obtained via the standard powerset construction. This construction can be lifted to coalgebraic generality, assuming a so-called Eilenberg-Moore distributive law between the functor termining the type of accepted structure (e.g.\ word languages) and a monad capturing the branching type (e.g.\ nondeterministic, weighted, probabilistic). Eilenberg-Moore-style coalgebraic semantics in this sense has been shown to be essentially subsumed by the more general framework of graded semantics, which is centrally based on graded monads. Graded semantics comes with a range of generic results, in particular regarding invariance and, under suitable conditions, expressiveness of dedicated modal logics for a given semantics; notably, these logics are evaluated on the original state space. We show that the instantiation of such graded logics to the case of Eilenberg-Moore-style semantics works extremely smoothly, and yields expressive modal logics in essentially all cases of interest. We additionally parametrize the framework over a quantale of truth values, thus in particular covering both the two-valued notions of equivalence and quantitative ones, i.e. behavioural distances.

cs.LO↗

arXiv2023

Quantitative Graded Semantics and Spectra of Behavioural Metrics

Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.

cs.LO↗

arXiv2022

Hennessy-Milner Theorems via Galois Connections

We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular this framework allows us to derive a new fixpoint characterization of directed trace metrics.

cs.LO↗

arXiv2022

Graded Monads and Behavioural Equivalence Games

The framework of graded semantics uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of infinite-depth graded semantics. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.

cs.LO↗

arXiv2019

Bisimulation maps in presheaf categories

The category of presheaves on a (small) category is a suitable semantic universe to study behaviour of various dynamical systems. In particular, presheaves can be used to record the executions of a system and their morphisms correspond to simulation maps for various kinds of state-based systems. In this paper, we introduce a notion of bisimulation maps between presheaves (or executions) to capture well known behavioural equivalences in an abstract way. We demonstrate the versatility of this framework by working out the characterisations for standard bisimulation, $\forall$-fair bisimulation, and branching bisimulation.

cs.LO↗

arXiv2017

Conditional Transition Systems with Upgrades

We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transition systems (LaTS), where transitions are labelled with the elements from a distributive lattice. We define equivalent notions of bisimilarity for both variants and characterise them via a bisimulation game. We explain how conditional transition systems are related to featured transition systems for the modelling of software product lines. Furthermore, we show how to compute bisimilarity symbolically via BDDs by defining an operation on BDDs that approximates an element of a Boolean algebra into a lattice. We have implemented our procedure and provide runtime results.

cs.SE↗

arXiv2017

On path-based coalgebras and weak notions of bisimulation

It is well known that the theory of coalgebras provides an abstract definition of behavioural equivalence that coincides with strong bisimulation across a wide variety of state-based systems. Unfortunately, the theory in the presence of so-called silent actions is not yet fully developed. In this paper, we give a coalgebraic characterisation of branching bisimulation in the context of labelled transition systems and fully probabilistic systems. It is shown that recording executions (up to a notion of stuttering), rather than the set of successor states, from a state is sufficient to characterise branching bisimulation in both cases.

cs.LO↗

arXiv2016

A coalgebraic treatment of conditional transition systems with upgrades

We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branching type of the coalgebra and investigate the resulting behavioural equivalence. Furthermore we show how an existing algorithm for coalgebra minimisation can be instantiated to derive behavioural equivalences in this setting.

cs.LO↗

arXiv2014

Spinal Test Suites for Software Product Lines

A major challenge in testing software product lines is efficiency. In particular, testing a product line should take less effort than testing each and every product individually. We address this issue in the context of input-output conformance testing, which is a formal theory of model-based testing. We extend the notion of conformance testing on input-output featured transition systems with the novel concept of spinal test suites. We show how this concept dispenses with retesting the common behavior among different, but similar, products of a software product line.

cs.SE↗