Deciding rational property definitions

Abstract

Language Equations is an area of Theoretical Computer Science that is concerned with expressing desirable constraints on formal languages of interest and answering algorithmic problems about such languages. Language Equations can be used as a means to express desirable properties a language can have. The LaSer system allows users to supply a regular language and a property described by a given transducer or trajectory, and return whether or not the language satisfes the given property. An important potential feature of LaSer is the ability to supply a rational language equation to LaSer, and allow it to decide this equation, that is, to test that the equation holds. This functionality has been implemented, and will be outlined in this paper.