Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Regular Model Checking for LTL(MSO)?

The date of receipt and acceptance will be inserted by the editor Abstract. Regular model checking is a form of sym-bolic model checking for parameterized and infinite-state systems whose states can be represented as words of ar-bitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal prop-erties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under considera-tion. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying tempo-ral properties. In addition, the first-order quantification in MSO can be used to express properties parameter-ized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a Büchi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of pa-rameterized algorithms from the literature