jMosel: A Flexible Tool-Set for Monadic Second-Order Logic on Strings

jMosel is a tool-set for the analysis and verification of linear para- metric systems in monadic second-order logic on strings. In this paper we concentrate on the presentation of the core tool which supports several input and output formats as well as the interchange of the tool-set's internal com- ponents. The main design principles of jMosel are its layered approach to the logic, the definition of a formal semantics for a minimal subset, its modular design and its integration into the jABC application design environment. The tool demonstration in the appendix shows how to use jMosel as a stand-alone tool and as a plugin for the jABC environment.