See also:

  • automata
  • regular expression
  • imperative proving
  • model checking

Breaking up into these categories is kind of arbitrary

Regular Expressions

See also note on automata

Thompson construction Finding minimum regex for given string (or set of strings). Identify groups within a given string Is this related to invariant inference I wonder?

Knuth morris pratt regular expression rewriting or optimization. Slightly difference from equivalence but related. Minimization

Z3 checking regex containment An SMT Solver for Regular Expressions and Linear Arithmetic over String Length cav’21

(declare-const a String)
;(assert ( "ab" ( "ab")))
(assert-not ( a ( "ab")))
(assert ( a (re.++ ( "a") (re.++ (re.* ( "b"))))))


compile regexp to C

Matching algorithms

  • backtracking search
  • convert to dfa

Matching is state inference perhaps of traces. Regular Expressions : Logic Programming :: DFA : Functional Programming

Brzozowski Derivatives Oh, that’s interesting u^-1 as a notation.

s in R <-> emp in s^-1 R This gives us a matching algorithm.

The final coalgebra is one that operates on sets of strings? from a regular expression, produce a regex for the family with one a stripped off. THis looks like a derivatve operation kind of because the sequence operator turns into a sum. Or a multiplicatve inverse. Brzozowski derivatives

type kleene = Lit of char | One | Zero | Star of kleene | Plus of kleene * kleene | Seq of kleene * kleene

let deriv a = function
| Lit a'  a' == a -> One
| -> Zero
| Star e -> Seq ((deriv e), Star e)
| Plus a b -> 
| Seq a b -> Assoc, Comm, and idempotency necessary to actually make finite automata. flattening, sorting, and deleting duplicates is enough. List.sort_uniq Might be an interesting egglog example

type prods = One | Lit of char | Star of prods | Seq of kleene * kleene
type kleene = seq list (* sum of product representation. Hmm. Is this actually possible? Star gets in the way *)

parsing with derivatives


regex equivalence can check containment of string. also regex containmnt a + b = a means b <= a one he says do the dumb rewrite rules. hmm. We could egglog these hopcroft karp examples.

See kleene algebra. This is an equational method for equivalence checking of regex expressions

Normal Forms are usually a good way of checking equivalence when you can. Automata are kind of a normal form


pumping lemma used to prove languages are not regular Whenever a sufficiently long string is accepted it must be in the same state twice Find an inifnite family of string that isn’t pumpable

myhill nerode theorem necessary and sufficient condition for languasge to be regular define an equivalence relation. Sort of this relation is defining a notion of observably different traces. If there is no suffix z where xz fails but yz accepts or vice versa, the strings x y are considered equivalent. These equivalence classes correspond to states in a minimal automata. Given the classes, I can append letters to them to find the transitions between classes. By the definition all the elements in the class have to go to the same other class, because they can’t be distinguished

characterizing NFA <-> DFA <-> regexp <-> regular grammars left regular or right regular. Linear production rules + always has to be on the left or right. swapping left and right may not be regular anymore. Regular grammar nonterminals can be considered states in an NFA

kleene algerba

“In 1991, Dexter Kozen axiomatized regular expressions as a Kleene algebra, using equational and Horn clause axioms.[34] Already in 1964, Redko had proved that no finite set of purely equational axioms can characterize the algebra of regular languages.[35]”

powerset construction

proof pearl regular expressions isabelle

MOnadic second order logic


See also note on Parsing regularexp

Determinization - turn nondeterministic automaton to deterministic

Computing regex from automata Kleene’s algorithm Tarjan’s algorithm Basic algorithm of going back an forth is simple. Consider edges to be labelable by regexs. regex is equal to simple 2 state automata then with 1 edge You can eliminate states by performing the product of their in and out edges. You can create states and edges by expanding the regexp. Sequence is a new intermiedtae state. alternate is two parall arrows

Myhill Nerode theorem Pumping Lemma

Automata minimization - Partition refinement Separate into separate sets those which are definitely distinguishable (the remaining in same partition may or may not be). Things that transition into distinguishable things are distinguishable from each other. This is finding the nerode congruence

Datalog partition refinement? Sets. Things definitely not in set.

DAWG - transitions are single labelled edges. Transitions are

Hopcroft and Karp’s algorithm for Non-deterministic Finite Automata fado

Finite Automata


finite set of states. Labelled transitions between. omega automata - ru on infinite rather than finite strings Buchi - visit accepting state infinitely often Rabin Rust implementation of Weighted Finite States Transducers. speech recognition and synthesis, machine translation, optical character recognition, pattern matching, string processing, machine learning, information extraction and retrieval

Tree Automata Tree Automata Techniques and Applications

E-Graphs, VSAs, and Tree Automata: a Rosetta Stone slides merge only rules

Tree Automata as Algebras: Minimisation and Determinisation

Are tree automata kind of like finite state folds?

Compare with term rewrting fomrulation of regulr DFA. Special q marker q1 a -> a q2 Translated to term rewriting q1(a(X)) -> a(q2(X)) Starts to look like a tree automata. Recognizing a string is a fold over it, big woop.

pushdown automata

“recursive function with variables over finite domain”

See also: parsing

Probablistic automata PFA Minimization vs reduction residual

APEX online demo.

PRISM STORM stormpy tutorial

2019 Comparison of Tools for the Analysis of Quantitative Formal Models


Register automata nominal automata Timed automata Symbolic automata quantum atuomata

nominal automata Learning Nominal Automata Automata learning huh ALF - abstract lerarning framework

Kleene Algebra

Kleene Algebras and Applications - Alexandra Silva OPLSS Kleene Algebras: Theory and Applications

KAT symkat ocaml Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests transition function using BDD. Generating automata using Brzowski’s derivative and classical. bdds + union find for language equivalence safa is a library for automata

#use "topfind";;
#require "symkat";;
module S = Safa.Make(Queues.BFS)
Automata algerbaic program anlaysis graphs and paths can be represent by taking the letters of the alphabet to representedges in the graph. The paths from a to b can be represented as a regex Tarjan’s algorithm “path expression problem” If you have the path expression, you can just intepret it to calculate program quantities.

Kleene algerba with tests MOdelling language for horn equational? Relative of Propositional Hoare Logic. Which is a neat idea on it’s own


GKAT guarded kleene with test Kleene algebra modulo theories hmm. guess invariants kat modulo rewriting?

On the Coalgebraic Theory of Kleene Algebra with Tests Automatic proof generaton via derivatives? That sounds neat. Chen and Pucella - coalgerba theory of KAT

Automated Reasoning in Kleene Algebra Prover9/Mace4

topkat incorrectess logic and kat popl22

NetKat - kat for network reasoning Kleene Algebra with Tests and Coq Tools for While Programs

syntax are kleene expressions / logic is kleene algebra manipulation. logic is algebra on steroids semantics are strings

algerbraic laws + leastness of fixed point

hmm. 2x2 matrices have a schur complement representation theorem. hmmm.

a <= b <-> a + b = b

Well, this is basically doable

(datatype K 
 (+ K K) ; choice
 (* K) ; iterate
 (# K K) ; sequence
(define a K)
(define b K)
(# (* a) b)
(: (+ One a) (+ One b))
(* (+ a b))

; idempotent semiring
(rewrite (+ e Fail) e)
(rewrite (+ e f) (+ f e))
(rewrite (+ e f)) ; assoc
(rewrite (+ e e) e)

(rewrite (: ))

; star is least fix point

(rewrite (: (+ One a) a) (* a))

efficient procesure - antichain doyen upto bis9mualtion bonchi-pous 2015

kleene algerab with tests Add booleans as subset of kleene stuff

if b then p else q = b;p + ~b;q while b do p = (b;p)* not b

booleans commute under seq

guarded semantics. a kleene command is every possible pre and post condition. sequence needs the bools to meet in the middle

(Bool K Bool)

propositional hoare logic. {b}p{c} = bp~c == 0 what does that mean? oooooh. b p not(c). Ok that’s neat.

Models Language models - just actions Trace models - interspersed with states in btwee relation models - relation compose, relation closure tropical semiring and convex polyhedra matrices over another kleene algerba

Process Alegebras

  • CCS Calculus of communicating systems - milner
  • CSP Communicating sequential systems - hoare
  • ACP ?
  • Pi-calculus

u-calc without the modal fixed point theory backhouse - galois connections and fixed point calculus

rules minimal set solution to constraint system

Monadic Second Order Logic Colorability Monadic = one entry of predicate We can quantify over them

What even is the category I should put MSO under? Automata? Logic? Model theory? Model checking? goo stuff

Buchi-Elgot-Trakhtenbrot Theorem Iff string is describably in MSO, it is regular

NP - existential monaid. For example graph coloring. Figuring out the collring given grahp is annoying.

S1S The monadic second order theory of N under successor

S2S Tree width, tree decompoistion courcelle’s theorem - tree wsth graphs can have mso formula decided in time

Monadic Second-Order Logic on Finite Sequences MSO for heap models


Petri Nets

Boolean Equation Systems

Boolean equations with fixed points. I don’t get it.

SOLVING BOOLEAN EQUATION SYSTEMS by translation to ASP? Verification of Modal Properties Using Boolean Equation Systems

mu and nu fixed oiutbs

parametrized BES kind of sounds like BES modulo theories.


BisPy is a Python library for the computation of the maximum bisimulation of directed graphs. I’m confused. Is it partition refinment or union find?

alogirhtmics of bisimulation

Of what relationship is bisimulation to non-interference proofs? Bisimulation is kind of a way of saying the state is unobservable from the actions/observations.

Graph isomorphism - too striog? Trace equivalence - Too strong?

There is a distinction between saying a given relation is a bisimulation and defining it to be a bisimilar closure of something.

Least vs greatest fixed point

Simulation Refinement of behavior


Data-Codata Symmetry and its Interaction with Evaluation Order Howw to design co-porgrams - gibbonsd - Classical (Co)Recursion: Programming Paul Downen, Zena M. Ariola, examples in python scheme, agda

codata is productive, meaning recursion is guarded by applications of constructors

copatterns Are copatterns simple? They just explain what to do on every application of an accessor functiojn on a record. This is the same thing as giving the record explicility altenrkirch coinduction in agda

Copatterns: programming infinite structures by observations


Coalgebra for the working programming languages researcher Coalgebraic Semantics [1/4] - Alexandra Silva - OPLSS 2019 Functor gives you syntax and semantics. denotationa and operational. Determinstic atuomatya F(X) = X^A = A -> X. so transition relation is X -> F(X) = X -> A -> X. If you icnlude termination (X->Bool,A -> X). Somehow the pieces of reg exp corespond to Final coalgebra gives a denotational semantics Brzowsksi derivatives give operational semantics.

Arbib and Manes - algerbad approaches to program semantics Rutten and Bart Jacobs

A coalgebra ia a pair (X,a) where a : X -> f X. This is somehow modelling automata. Very weird right? Conceptually X is the set of states, F describes the schema of data/automata type, and a is a functional (dictionary) description of the transition graph. Modelling in this way is somehow stating that every node/state has a “uniform” structure/edges F associated with it. The dictionary is the “successor” map. But if X and a are considered opaque, how do you describe the automata in pure categorical terms? Well, the category ish way of talking about Set is to use morphisms from unit to pick out elements. So a particular automata will be described by a set of equations on the morphism a. Morphisms between coalgebras are automata mappings. (Simulations?) category theory in python 4. What is finding the minimization of an automata categorically.

An specific algebra is the analog of an intepretation. Some interpretations are models of the axioms and some aren’t Consider finite groups. What are the equations of an algerbaic structure interpreted categorically.

# x + x*x -> x
# f(x) = x + x*x 
alg = {
  ("plus",1,2) : 3,
  ("plus",4,5) : 9,
  ("num", 4) : 4

def map_F(f,x):
  match x:
    case ("plus",x,y):
      return ("plus", f[x],f[y])
    case ("num",z):
      return ("num",z)

# lift map over dict also
def map2(f,x):
  return { map_F(f,k) : v  for k,v in x.items()}

# start at minimally identified rather than maximally identified
eqclass0 = {i:i for i in range(1000)}
#eqclass0 = {} # or empty? Void -> Id rather than Id -> ()
print(map2(eqclass0, alg))
for n in range(10):
# (c -> a) -> (f a -> b) -> f c -> b
#  f l = \fc -> l (map f fc) 

The analog/dual of automata minimization is probably congruence closure. This jives nicely. The signature is the choice of functor. Refactoring the entire egraph into a single dictionary. That’s elegant.

Jules Jacobs, Thorsten Wißmann - Different automata types can be described by a Functor, meaning a function or dictionsry from states to something that may also involve states.

FOr exmaple, labbleled transition systems might be Map<State, Map<Action, State>>, non deterministic systems.

Or in other words (?) various kinds of automata graphs can be encoded as a functions from nodes to the outgoing edges. This isn’t really saying all that much. But the structure/type of the function/dict can enforce certain regularity properties of the graph.

Observational equivalence is obtained by considering the properties to be observable.

f(x) = 7
g(x) = "foo"

f(y) = 7
g(y) = "foo"

If f and g are the only pieces of data obervable of these opaque objects, then x and y are observationally equvalent. Interestingly, by even posing the question, I was stating some meta sense in which x and y are not equivalent

If the identifiers become observations, now x and y aren’t equivalent

f(x) = 7
g(x) = "foo"
name(x) = "x"

f(y) = 7
g(y) = "foo"
name(y) = "y"

It gets more interesting when we say that there are observations that are themselves the opaque objects.

f(x) = 7
g(x) = "foo"
next(x) = y

f(y) = 7
g(y) = "foo"
next(y) = x

Now are they equivalent? It isn’t so clear. A possible definition and method is to sort of back up obervable differences and propagate them. If two things map into two distinguishable things, they are also distinguishable. ob(x) != obs(y) -> x != y. This is the contrapositive of congruence.

This process breaks identifiers into equivalence classes. The equivalence classes can be naturally labelled by the observations themselves.

The map id -> f id describes the automata. f is a functor, hence has a notion of map. Because of this, given a emap : id -> eqclass mapping we can get id -> f eqclass. I am however suggesting that eqclass is some kind of fix of f applied to (). eclass0 = (). eclass1 = f () emap0 = fun _ -> (). eclass is Free f. If we hash cons, eclass ~ int.

Here’s the simple naive algorithm. The paper covers essential optimizations. Something like the analog of seminiave evaluation and also good choice of eclass ids.

ex1 = {
  1 : (False, 2, 3),
  2 : (False, 4, 3),
  3 : (False, 5, 3),
  4 : (True, 5, 4),
  5 : (True, 4, 4)

def dfa_map(f,x):
  return {n : (term, f[a], f[b])  for n, (term, a, b) in x.items()}

eqclass = {i : () for i in range(1,6)}
for _ in range(10):
  eqclass = dfa_map(eqclass, ex1)
  #eqclass = {k : hash(v) for k,v in eqclass.items()} # not quite right. hash could collide. But you get the idea
  statelabel = { k : -i-1 for i,k in enumerate(set(eqclass.values()))} # negative just so I can see different between state and eqclass easier
  eqclass = {k : statelabel[v] for k,v in eqclass.items()} 



What if I Z3-ified this process? A symbolic transition map. eqclass(c) = a.
Could use same justification tricks.



Coinduction. What up?

coinduction he nice blog post. Greatest fixed point takes everything and prunes away stuff that can’t be proven. Least fixed point starts with nothing an adds stuff that can be proven.

bisimulation graph isomorphism between two systems is too strong. Why? it only requires that each system has some way of finding corresponding states.

What is induction really?



Verification Anything fun? Puzzles? Program alignment?


boa tool CoPaR Generic Partition Refinement and Weighted Tree Automata CoPaR: An Efficient Generic Partition Refiner DCPR are similar tools in some sense

CADP LOTOS format. Explicit vs implicit LTS tutorial boolean equation systems. CAESAR tool


VLTS very large transition system bnenchmark suite BEEM: BEnchmarks for Explicit Model Checkers

circ K


user manual mCRL2. Hmm. Impressive. ucrl2 language LPS format.

  • mcrl2-gui
  • ltsgraph tool to visualize
  • lpsim to simualte
  • ltsconvert - reduce an lts modulo equivalence

parametrised boolean equation systems modal u-calculus

Vending machine

  ins10, optA, acc10, putA, coin, ready ;
  User = ins10 . optA . User ;
  Mach = acc10 . putA . Mach ;
    { coin, ready },
      { ins10|acc10 -> coin, optA|putA -> ready },
      User || Mach
  ) ) ;

sort Nat;
cons zero : Nat;
successor : Nat —> Nat,

coursera course labelled transition system

import os
os.system("echo try this")

Partition Refinement

Model Checking

Should this be in here? See also:

  • imperative proving
  • constrained horn clauses

  • SPIN, promela
  • TLA+
  • KIND
  • ProB
  • FDR
  • nusmv


modelc checking contest petri nets? Not seeing familiar systems here hardware model checkers contest

  • AVR
  • abc
  • Pono


    Automata theory - An algorithmic approach book. Wait this seems fantastic. BDD as a kind of automata. solving presburger arith by reduction to automata? Bizarre.

Automata : From Logics to Algorithms - Vardi and Wilke

Hopcroft and Ullman book wolfgang thomas autmata logic and games High performance Trie and Ahocorasick automata (AC automata) Keyword Match & Replace Tool for python

Automatalog partially built objects just can have fewer entries. But then how do we inform pointer to the objects they gave been nondestructive update Monotonically, observations go down, equalities go up. observations go up, equalities go down. We can remove obserations and stay monotonic with respect to equality. Horizontal strtification. Relationship with subclassing? first strata of most fine-grained class rules. object oriented databases Rows ~ objects, observations ~ fields. Record vs copattern defnition of codata. Open automata that havn’t been filled out, have incomplete observations, or observations with partial equality, or lattice observations. We cannot compress these. We must consider observations that could possibly be distinguishable as distinguishable. Can we force equalities? codeql is an object oriented shellac on datalog logtalk weighted automata perform a merge like operation when states combine? “lumping” Options:

  • When a subobservation completes (if objects are stable) it splits the universe.
  • when incompatbile observations occur, split. modal u-calc is a fixpoint algebra yihong said datalog is equation solving tree automata and egglog.

higher dimensional automata pratt woof. What even is this.

[POPL’22] Coalgebra for the working programming languages researcher

A pointery circular list is a labelled transition system if which node you’re on is the state, and tail takes you to the nexxt state and head is an action that takes you to the same state. Two observationally eqauivalnt cirucils lists ones = 1 : 1 : ones and ones = 1 : ones are bisimilar

A more natural definition is observation O, S states, A actions. head would then be an observation on the state.

Egraphs as transition systems? Observations of head, argument choice as action? This suggests we don’t have to canonicalize it?

The existential form of a coinduccutive type exists s, (s, s -> f s) Is the analog of a closure form exists s. (s, (s,a) -> b) We can defunctionalize the possible states and put all the s -> f s things in the apply function?

Ones Inc1 n

apply (Inc1 n) = Cons a (Inc1 (1 + n)) A closed data type of all my possible streams


bisimulation goes hand in hand with condicution.

What does it mean for two systems to be equal?

Automata traditionally just worry about the trace they accept. Nodes are labelled with somethign and edges are labelled with somethign. not persay atomic actions.

Hmm. So the record type condictive in coq. Each accessor is a message or action And I suppose each value of the conidcutive is a state. Is this a bisimulation under that understanding?

CoInductive bisim {A : Set} (x y : stream A) : Set :=
  | bisim_eq : head x = head y -> bisim (tail x) (tail y) -> bisim x y. - lusxia - shows an interesting defunctionalization trick to define fix. Is the point to close the universe of possible functions so that coq can see that we’re only using productive ones interaction trees conor mcbride turing completeness

A process in coq. The labelled trasnition relation. Ok sure. Inductive trans s1 a s2 :=

Then what? Definition bisim ta tb sa1 sa2 := forall s1 Definition IsBisim r ta t2 := forall sa1

Sangiorgi Book

Connection to recursion schemes. Categorical perspective. Meijer.

“Biggest Fixed Point”

a -> f a building up a functor f

f a -> a breaking down a functor f

Coinduction ~ object oriented. Observations / messages are sent to a data object Existential encoding - Strymonas paper exists s, {state : s ; observation1 : s -> yada ; observation2 : s -> yada } As compared to universal encoding (Bohm berarducci) of inductive types (their fold)

LogTalk - Co-LP (logic programming), rational trees. Could one fold together the lambda prolog perspective and a talk by gupta Vicisou Circle - book Aczel in 80s?

Co-LP is dual to tabling The metinterpeter looks very simple. What is a metaintepreter for tabling. Is it similarly simple? Keep list of previous calls. Attempt to unify with a previous call. This recognizes cycles. co-auto for Coq? Does paco do something like this? Interesting connection: Sequent as a virtual machine, lambnda prolog sequents describe logic programming, This coniductive metainterpreter reifies the goal stack. So does the delmittied continuation based tabling. Coinductive = negative types Sequent calc as a virtual machine is already kind of how lambda prolog is described. But Downen was talking classical logic, and Miller nadathur almost exclusively constructive logic. Miller and nadathur do have function types, distinct from implication (I think). Could one make a prolog on this basis. Should the coinductive predicates somehow be connected to continuations? The tabled version reifies a goal stack for delimitted continuations. No wait. I’m remembering achieving tabling via delimitted conts.

< | > :- < | >, < | > Or this as a notation for callcc, shift/reset? In scheme or whatever the conitnuation is not omnipresent in notation. p(X,Y) :- < K | > % this is binding a K with callCC or something Downen and Ariloa are saing classical logic does have an operational semantics, some what maybe in contradictin to the feel of what Miller is saying,. Co-Logic Programming: Extending Logic Programming with Coinduction L. Simon, A. Mallya, A. Bansal, G. Gupta

Downen. Connections back to sequent calculus papers. Computing with classical connectives.

Bisimulation Coinductive proof

Coq and coidnuction Chlipala’s chapter Breitner blog post -

Older notes - Nice ones by Eduardo Giménez and Pierre Castéran (2007). “A Tutorial on [Co-]Inductive Types in Coq” Paco Computability theory library

Basic interesting proofs:

techniques - unfold via a match function. Condinductive records are smarter? Positive and negative types metric donictuction What is this practical coinduction - kozen Interactive programming Agda - Objects and GUIs.

The smallest coinductive is unit The smallest inductive is void

Finite enum types = inductives

Mixing in enums, you can make finite product types as coindcutives.

Taking it more hard core, you could make a record for every body of an inductive.

Primitive inifinite condinductive is Forever primitive infiniter indcutive is nat

Negative types and positive types. They come together to create activity. Push streams and pull streams

Neel - Hi, this is a surprisingly complicated question. For lazy languages, least and greatest fixed points coincide. (The jargon is “limit-colimit coincidence” or “bilimit-compactness”.) For strict languages, they do not coincide, and while you can still encode them, the absence of coinductive types is arguably a language deficiency. For languages with first class continuations, they are perfect duals – the negation of an inductive type is a coinductive type, and vice versa. This also means that the eliminator for an inductive value is a coinductively defined continuation, and vice versa. (See David Baelde’s Least and Greatest Fixed Points in Linear Logic.) This duality does not hold in languages without first class continuations, since there is an asymmetry between how you can use values and how you can use continuations. You will sometimes see people talking about how inductive types are strict and coinductive types are lazy. This is a misconception – in a language with continuations, you can have both strict and lazy inductive types, and strict and lazy coinductive types. Due to the aforementioned asymmetry, in a language withouts control, you can have strict and lazy inductives, but only lazy coinductive types. (This is in Baelde’s paper, but you have to squint to realize it, because he was doing proof theory rather than language design.) Balede’s paper