arXiv 1007.37692010-07cs.LO

Non-Deterministic Kleene Coalgebras

Alexandra Silva, Marcello Bonsangue, Jan Rutten

发表信息：: Logical Methods in Computer Science, Volume 6, Issue 3 (September 9, 2010) lmcs:695
DOI：: 10.2168/LMCS-6(3:23)2010

英文摘要：

In this paper, we present a systematic way of deriving (1) languages of (generalised) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of systems. This generalizes both the results of Kleene (on regular languages and deterministic finite automata) and Milner (on regular behaviours and finite labelled transition systems), and includes many other systems such as Mealy and Moore machines.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

带检验的Kleene代数的余代数方法

A Coalgebraic Approach to Kleene Algebra with Tests

带有测试的Kleene代数是Kleene代数（正则表达式代数）的扩展，可用于推理程序。我们开发了一个coalgebraic理论的Kleene代数测试，沿线的coalgebraic理论的正则表达式的基础上确定性自动机。由于已知的自动机理论表示的Kleene代数与测试不借给自己的一个coalgebraic理论，我们定义了一个新的解释Kleene代数与测试表达式和相应的自动机理论表示。该理论的一个成果是一个共归纳证明原理，它可以用来建立我们的Kleene代数与测试表达式的等价性。

2004-05-26cs.LOcs.PL

Automatic Equivalence Proofs for Non-deterministic Coalgebras

A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analogue of Kleene's theorem and Kleene algebra, were recently proposed by a subset of the authors of this paper. Examples of the systems covered include infinite streams, deterministic automata, Mealy machines and labelled transition systems. In this paper, we present a novel algorithm to decide whether two expressions are bisimilar or not. The procedure is implemented in the automatic theorem prover CIRC, by reducing coinduction to an entailment relation between an algebraic specification a…

2013-03-11cs.FLcs.LO

正则与$\omega$-正则行为的上代数视角

A coalgebraic take on regular and $ω$-regular behaviours

本文提出一个上代数框架，用单子定义有限和无限行为，并给出上代数Kleene型定理，适用于非确定性、树和概率自动机。

2021-12-22cs.LO

Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages

We introduce a generic expression language describing behaviours of finite coalgebras over sets; besides relational systems, this covers, e.g., weighted, probabilistic, and neighbourhood-based system types. We prove a generic Kleene-type theorem establishing a correspondence between our expressions and finite systems. Our expression language is similar to one introduced in previous work by Myers but has a semantics defined in terms of a particular form of predicate liftings as used in coalgebraic modal logic; in fact, our expressions can be regarded as a particular type of modal fixed point fo…

2018-05-14cs.LO

Coalgebraic Semantics for Nominal Automata

This paper provides a coalgebraic approach to the language semantics of two types of non-deterministic automata over nominal sets: non-deterministic orbit-finite automata (NOFAs) and regular nominal non-deterministic automata (RNNAs), which were introduced in previous work. While NOFAs are a straightforward nominal version of non-deterministic automata, RNNAs feature ordinary as well as name binding transitions. Correspondingly, words accepted by RNNAs are strings formed by ordinary letters and name binding letters. Bar languages are sets of such words modulo $α$-equivalence, and to every stat…

2022-03-29cs.LO

Generalizing determinization from automata to coalgebras

The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. Fo…

2013-03-01cs.LO

更多相关论文收起更多论文

Coalgebraic Determinization of Alternating Automata

Coalgebra is a currently quite active field, which aims to look at generic state-based systems (most prominently automata) from a very abstract point of view, mainly using tools from category theory. One of its achievements is to give a completely generic approach of determinization, unifying in an elegant manner non-deterministic automata, probabilistic automata or non-deterministic pushdown automata in one and the same model. However, the case of alternating automata fails to easily fit in this model. The aim of this internship was therefore to tackle this problem: can alternating automata a…

2018-04-07cs.LO

Two modes of recognition: algebra, coalgebra, and languages

The aim of the paper is to build a connection between two approaches towards categorical language theory: the coalgebraic and algebraic language theory for monads. For a pair of monads modelling the branching and the linear type we defined regular maps that generalize regular languages known in classical non-deterministic automata theory. These maps are behaviours of certain automata (i.e. they possess a coalgebraic nature), yet they arise from Eilenberg-Moore algebras and their homomorphisms (by exploiting duality between the category of Eilenberg-Moore algebras and saturated coalgebras). Giv…

2019-06-13cs.FLcs.LO

Systematic Construction of Temporal Logics for Dynamical Systems via Coalgebra

Temporal logics are an obvious high-level descriptive companion formalism to dynamical systems which model behavior as deterministic evolution of state over time. A wide variety of distinct temporal logics applicable to dynamical systems exists, and each candidate has its own pragmatic justification. Here, a systematic approach to the construction of temporal logics for dynamical systems is proposed: Firstly, it is noted that dynamical systems can be seen as coalgebras in various ways. Secondly, a straightforward standard construction of modal logics out of coalgebras, namely Moss's coalgebrai…

2012-12-07cs.LO

A New Foundation for Finitary Corecursion and Iterative Algebras

This paper contributes to a theory of the behaviour of "finite-state" systems that is generic in the system type. We propose that such systems are modelled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor is finitary and preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius,…

2019-09-06cs.LO

Structural operational semantics for non-deterministic processes with quantitative aspects

General frameworks have been recently proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions), aiming to provide general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition relation as…

2015-06-30cs.LO

Regular Expression Matching and Operational Semantics

Many programming languages and tools, ranging from grep to the Java String library, contain regular expression matchers. Rather than first translating a regular expression into a deterministic finite automaton, such implementations typically match the regular expression on the fly. Thus they can be seen as virtual machines interpreting the regular expression much as if it were a program with some non-deterministic constructs such as the Kleene star. We formalize this implementation technique for regular expression matching using operational semantics. Specifically, we derive a series of abstra…

2011-08-16cs.LO

GSOS for non-deterministic processes with quantitative aspects

Recently, some general frameworks have been proposed as unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions), aiming to provide general results and tools. This paper provides two contributions in this respect. First, we present a general GSOS specification format (and a corresponding notion of bisimulation) for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the ULTraS model, an extension of the usual LTSs where the transition rel…

2014-06-09cs.LOcs.PL