Find all traces satisfying a set of linear temporal logic (LTL) formulas

73 Views Asked by At

I want to compute all finite traces up to a given length that satisfy a set of linear temporal logic formulas. Does such an algorithm exist?

1

There are 1 best solutions below

1
On

The set of finite words satifying a given LTL formula is a regular (and even star-free) language and there are known algorithms to convert a LTL formula into, say, a deterministic automaton accepting the corresponding language. Next the set of words up to a given length $n$ of a regular language $L$ of $A^*$: it is the intersection of $L$ with $(1 + A)^n$ and again there are known algorithms to compute the intrersection of two regular languages.