Titlebook: Computer Aided Verification; 8th International Co Rajeev Alur,Thomas A. Henzinger Conference proceedings 1996 Springer-Verlag Berlin Heidel

Harass

FER

Computer Aided Verification978-3-540-68599-9Series ISSN 0302-9743 Series E-ISSN 1611-3349

RENIN

https://doi.org/10.1007/978-3-662-48599-6 sets as the common zeros of sets of polynomials. This approach could serve as a useful supplement to symbolic model checking methods based on Ordered Binary Decision Diagrams and may provide important theoretical insights by bringing the powerful mathematical machinery of algebraic geometry to bear on the model checking problem.

叫喊

https://doi.org/10.1007/978-3-658-11406-0on labelled transition systems extended to the probabalistic setting and gives an .(n2·m) algorithm for testing probabilistic bisimulation and an . (....) algorithm for testing probabilistic simulation where . is the number of states and . the number of transitions in the underlying probabilistic transition systems.

外来

LIEN

Die Grundlagen der Untersuchung,We develop a HORNSAT-based methodology for verification of finite state systems. This general methodology leads naturally to algorithms, that are local [25, 19], . [28, 11, 13, 5] and . [24]. It also leads naturally to . behavioral relation checking

招惹

HORNSAT, model checking, verification and games,We develop a HORNSAT-based methodology for verification of finite state systems. This general methodology leads naturally to algorithms, that are local [25, 19], . [28, 11, 13, 5] and . [24]. It also leads naturally to . behavioral relation checking

灯丝

Symbolic model checking using algebraic geometry, sets as the common zeros of sets of polynomials. This approach could serve as a useful supplement to symbolic model checking methods based on Ordered Binary Decision Diagrams and may provide important theoretical insights by bringing the powerful mathematical machinery of algebraic geometry to bear on the model checking problem.

集合

Polynomial time algorithms for testing probabilistic bisimulation and simulation,on labelled transition systems extended to the probabalistic setting and gives an .(n2·m) algorithm for testing probabilistic bisimulation and an . (....) algorithm for testing probabilistic simulation where . is the number of states and . the number of transitions in the underlying probabilistic transition systems.

Congeal

Pushdown processes: Games and model checking,winning strategy which is realized by a pushdown process. This fact turns out to be connected with the model checking problem for push-down automata and the propositional .-calculus. It is show that this model checking problem is DEXPTIME-complete.