We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic. © 2013 World Scientific Publishing Company.
Automated termination in model-checking modulo theories / Carioni, A.; Ghilardi, S.; Ranise, S.. - In: INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE. - ISSN 0129-0541. - 24:2(2013), pp. 211-232. [10.1142/S012905411340008X]
Automated termination in model-checking modulo theories
Ranise S.
2013-01-01
Abstract
We identify sufficient conditions to automatically establish the termination of a backward reachability procedure for infinite state systems by using well-quasi-orderings. Besides showing that backward reachability succeeds on many instances of problems covered by general termination results, we argue that it could predict termination also on interesting instances of the reachability problem that are outside the scope of applicability of such general results. We work in the declarative framework of Model Checking Modulo Theories that permits us to exploit recent advances in Satisfiability Modulo Theories solving and model-theoretic notions of first-order logic. © 2013 World Scientific Publishing Company.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione