Name
Abstract | ||
|---|---|---|
We present a model checking algorithm for HFL1, the firstorder fragment of Higher-Order Fixpoint Logic. This logic is capable of expressing many interesting properties which are not regular and, hence, not expressible in the modal µ-calculus. The algorithm avoids best-case exponential behaviour by localising the computation of functions and can be implemented symbolically using BDDs. We show how insight into the behaviour of this procedure, when run on a fixed formula, can be used to obtain specialised algorithms for particular problems. This yields, for example, the competitive antichain algorithm for NFA universality but also a new algorithm for a string matching problem. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-75560-9_7 | LPAR |
Keywords | Field | DocType |
first-order fragment,higher-order fixpoint logic,specialised algorithm,exponential behaviour,algorithm avoids,fixed formula,nfa universality,model checking algorithm,firstorder fragment,new algorithm,competitive antichain algorithm,higher order,model checking,string matching,first order | String searching algorithm,Modal μ-calculus,Antichain,Model checking,Computer science,Algorithm,Theoretical computer science,Modal logic,Fixed point,Tree automaton,Computation | Conference |
Volume | ISSN | ISBN |
4790 | 0302-9743 | 3-540-75558-6 |
Citations | PageRank | References |
5 | 0.46 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roland Axelsson | 1 | 49 | 3.44 |
| Martin Lange | 2 | 34 | 2.63 |