Property Pattern Mappings for LTL: Existence

Pattern: K occurs

[ Globally ] [ Before M ] [ After L ] [ Between L and M ] [ After L Until M ]

Globally

0	<> K
1	<> K
2	<> / K
3	<> / K

Before M

0	<> M -> ( K P M )
1	<> / M -> ( ! / M U K )
2	<> M -> ( / K P M )
3	<> / M -> ( / K P / M )

After L

0	<> L -> <> ( L && <> K )
1	<> / L -> <> ( / L && o <> K )
2	<> L -> <> ( L && <> / K )
3	<> / L -> <> ( / L && <> / K )

Between L and M

0	[] (( L && <> M ) -> (( K P M ) && ! M ))
1	[] (( / L && <> / M ) -> ( o ( ! / M U K ) && ! / M ))
2	[] (( L && <> M ) -> (( / K P M ) && ! M ))
3	[] (( / L && <> / M ) -> (( / K P / M ) && ! / M ))

After L Until M

0	[] ( L -> ( if <> M then ( ( K P M ) && ! M ) else <> K ) )
1	[] ( / L -> o ( ! / M U K ) && ! / M )
2	[] ( L -> ( if <> M then ( ( / K P M ) && ! M ) else <> / K) )
3	[] ( / L -> ( if <> / M then ( ( / K P / M ) && ! / M) else <> / K ) )

Back to the Property Pattern Mappings for LTL