Regular Model Checking

Regular Model Checking" (or "RMC") is a uniform framework for algorithmic verification of infinite-state systems. In RMC, states are represented by words over a finite alphabet, and transitions are are represented by finite-state transducers. Regular Model Checking" (or "RMC") is a uniform framework for algorithmic verification of infinite-state systems. In RMC, states are represented by words over a finite alphabet, and transitions are are represented by finite-state transducers.