Titlebook: Computer Aided Verification; 6th International Co David L. Dill Conference proceedings 1994 Springer-Verlag Berlin Heidelberg 1994 Automate

摇摆

Model checking of macro processes,se decision procedures handle correctly also process systems which are defined by unguarded recursion. As expected, the worst case complexity depends on the highest type level in the process description, and it is .-exponential in the size of the formula for a system description with type level ..