%0 Journal Article %1 aziz2004regular %A Abdulla, Parosh Aziz %A Jonsson, Bengt %A Nilsson, Marcus %A d’Orso, Julien %A Saksena, Mayank %D 2004 %J Computer Aided Verification %K distributed modelchecking regular %P 348--360 %T Regular Model Checking for LTL(MSO) %U http://www.springerlink.com/content/r44p1huwv6gp1uux %X Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary 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 properties to be verified in regular model checking. 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 temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized 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) transducer 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 parameterized algorithms from the literature. ER -

@article{aziz2004regular, abstract = {Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary 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 properties to be verified in regular model checking. 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 temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized 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) transducer 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 parameterized algorithms from the literature. ER -}, added-at = {2009-11-13T18:25:30.000+0100}, author = {Abdulla, Parosh Aziz and Jonsson, Bengt and Nilsson, Marcus and d’Orso, Julien and Saksena, Mayank}, biburl = {https://www.bibsonomy.org/bibtex/2ddeb047b97ffe2340a17d74e25a67738/giuliano.losa}, description = {Regular model checking for LTL(MSO)}, interhash = {f49489d49180452fac29c514e0048d18}, intrahash = {ddeb047b97ffe2340a17d74e25a67738}, journal = {Computer Aided Verification}, keywords = {distributed modelchecking regular}, pages = {348--360}, timestamp = {2009-11-13T18:25:30.000+0100}, title = {Regular Model Checking for LTL(MSO)}, url = {http://www.springerlink.com/content/r44p1huwv6gp1uux}, year = 2004 }