Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

24

SPIN
2007
Springer

favoriteEmaildiscussreport

98views Theoretical Computer Science» more SPIN 2007»

Minimal Counterexample Generation for SPIN

14 years 5 months ago

Minimal Counterexample Generation for SPIN

Download www.student.cs.uwaterloo.ca

We propose an algorithm to compute a counterexample of minimal size to some property in a ﬁnite state program, using the same space constraints than SPIN. This algorithm uses nested breadth-ﬁrst searches guided by a priority queue. It works in time O(n2 log n) and is linear in memory.

Paul Gastin, Pierre Moro

Real-time Traffic

Algorithm | Minimal Size | SPIN 2007 | Theoretical Computer Science | ﬁnite State Program |

claim paper

Related Content

» Minimization of Counterexamples in SPIN

» Counterexample Explanation by Anomaly Detection

» Generating CounterExamples Through Randomized Guided Search

» Generation of All CounterExamples for PushDown Systems

» SubsumerFirst Steering Symbolic Reachability Analysis

» Teleoperation of Steerable Needles

» Graph Coloring and the Immersion Order

» Data Flow Testing as Model Checking

» Erratum to Reformulating table constraints using functional dependencies an application t...

Post Info
More Details (n/a)

Added	09 Jun 2010
Updated	09 Jun 2010
Type	Conference
Year	2007
Where	SPIN
Authors	Paul Gastin, Pierre Moro

Comments (0)