Testing SPIN's LTL Formula Conversion into Büchi Automata with Randomly Generated Input.

Heikki Tauriainen Keijo Heljanko

Published in: SPIN (2000)

Keyphrases

randomly generated
linear temporal logic
np complete
branch and bound algorithm
deterministic automata
boolean functions
model checking
finite automata
phase transition
cellular automata
lower bound
temporal logic
stochastic local search
satisfiability problem
boolean satisfiability
linear programming
upper bound