%0 Journal Article 
%F fmsd13
%A Bertrand, N.
%A Schnoebelen, Ph.
%T Computable fixpoints in well-structured symbolic model checking
%J Formal Methods in System Design
%V 43
%N 2
%P 223-267
%X We prove a general finite-time convergence theorem for fixpoint expressions over a well-quasi-ordered set. This has immediate applications for the verification of well- structured systems, where a main issue is the computability of fixpoint expressions, and in particular for game-theoretical properties and probabilistic systems where nesting and alternation of least and greatest fixpoints are common
%U http://www.irisa.fr/sumo/Publis/PDF/fmsd13.pdf
%U http://dx.doi.org/10.1007/s10703-012-0168-y
%8 October
%D 2013