Linear logic automata Original Research Article

A Linear Logic automaton is a hybrid of a finite automaton and a non-deterministic Petri net. LL automata commands are represented by propositional Horn Linear Logic formulas. Computations performed by LL automata directly correspond to cut-free derivations in Linear Logic. A programming language of LL automata is developed in which typical sequential, non-deterministic and parallel programming constructs are expressed in the natural way. All non-deterministic computations, e.g. computations performed by programs built up of guarded commands in the Dijkstraʹs approach to non-deterministic programming, are directly simulated within the framework of Linear Logic automata, and thereby within the Horn framework of Linear Logic.