Property Pattern Mappings for LTL: Response

Pattern: K responds to N

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

Globally

0	[] ( K -> <> N )
1	[] ( K -> <> N )
2	[] ( / K -> <> / N )
3	[] ( / K -> <> / N )

Before M

0	<> M -> ( K -> ( ! M U N ) ) U M
1	<> / M -> ( ( K -> ( ! / M U N ) ) && ! / M ) U ( / M && ( K -> L ) )
2	<> M -> ( / K -> ( ! M U / N ) ) U M
3	<> / M -> ( ( / K -> ( ! / M U / N ) ) U / M )

After L

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

Between L and M

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

After L until M

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

Back to The Property Pattern Mappings for LTL