Property Pattern Mappings for LTL: Precedence

Pattern: K precedes N

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

Globally

0	<> K -> N P K
1	<> K -> N P K
2	<> / K -> / N P / K
3	<> / K -> / N P / K

Before M

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

After L

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

Between L and M

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

After L until M

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

Back to The Property Pattern Mappings for LTL