Property Pattern Mappings for LTL: Absence

Pattern: K is absent

[ 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 U M )
1	<> / M -> ( / M P K )
2	<> M -> ( ! / K U M )
3	<> / M -> ( ! / K U / M )

After L

0	[] ( L -> [] ! K )
1	[] ( / L -> o [] ! K )
2	[] ( L -> [] ! / K )
3	[] ( / L -> [] ! / K )

Between L and M

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

After L until M

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

Back to The Property Pattern Mappings for LTL