A Rooted Tableau for BCTL*

Relatore:  John McCabe-Dansted - University of Western Australia
  giovedì 3 novembre 2011 alle ore 16.30 16:30 inizio seminario

The existing pure tableau technique for satisfiability
checking BCTL* [MarkReynolds02012007] begins by constructing all
possible colours. Traditional tableaux begin with a single root node,
and only construct formulae that are derived from that root. These
rooted tableaux provide much better performance on most real world
formulae, as they only need to construct a fraction of the possible
nodes. We present a rooted variant of this tableau for BCTL*, together
with an implementation demonstrating the performance of our rooted
variant is superior to the original; this implementation is made
available as a Java applet. We discuss further possible optimisations.
This research will be useful in finding an optimised rooted tableau
for CTL*.


Referente
Davide Bresolin

Referente esterno
Data pubblicazione
1 novembre 2011

Offerta formativa

Condividi