Search
Browse
Shopping Cart
Upload
Settings
Help
Previous Version
Sorted by
State Size
Formula Length
Temporal Hierarchy
Spec Patterns
Refresh
Filtered by
Automaton Type
Select
/
Deselect
All
NBW
DBW
NGBW
DGBW
NCW
DCW
NMW
DMW
NRW
DRW
NSW
DSW
NPW
DPW
State Size
Select
/
Deselect
All
1 state
2 states
3 states
4 states
5 states
More than 5 states
Formula Length
Select
/
Deselect
All
No temporal formulae
1 temporal operator
2 temporal operators
3 temporal operators
4 temporal operators
More than 4 operators
Temporal Hierarchy
Select
/
Deselect
All
To Be Determined
SafeGuarantee
Safety
Guarantee
Obligation
Recurrence (Response)
Persistence
Reactivity
Spec Patterns
Select
/
Deselect
All
Unknown
Absence
Universality
Existence
Bounded Existence
Precedence
Response
Precedence Chain
Response Chain
Constrained Chain Patterns
Refresh
Grouped By
Language Class
Refresh
<< First page
< Pre
12
13
14
15
16
[17]
18
19
20
21
22
Next >
Last page >>
241 - 255 / 395; page
/ 27
¬ G (p → F (q ∧ F r))
Equivalent:
F (p ∧ G (¬ q ∨ G ¬ r))
•
¬ G (p → F (q ∧ F r))
Complement:
G (p → F (q ∧ F r))
NBW
G (p → F G q)
Equivalent:
F G (O p → q)
•
G (p → F G q)
Complement:
F (p ∧ G F ¬ q)
•
¬ F G (O p → q)
•
¬ G (p → F G q)
•
G F (O p ∧ ¬ q)
NBW
¬ G (p → G (q → F r))
Equivalent:
¬ G (p → G (q → F r))
•
F (p ∧ F (q ∧ G ¬ r))
Complement:
G (p → G (q → F r))
NBW
¬ (F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r)))
Equivalent:
¬ (F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r)))
•
F p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))) W (p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))))
Complement:
F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))
NBW
¬ G (p → F (q ∧ X F r))
Equivalent:
¬ G (p → F (q ∧ X F r))
Complement:
G (p → F (q ∧ X F r))
NBW
F G a ∧ G F q
Equivalent:
F G a ∧ G F q
Complement:
NBW
X a ∧ G (a → X X a)
Equivalent:
X a ∧ G (a → X X a)
Complement:
NBW
G (Q ∧ ¬ R ∧ F R) → (P → ¬ R U (S ∧ ¬ R)) U R
Equivalent:
G (Q ∧ ¬ R ∧ F R) → (P → ¬ R U (S ∧ ¬ R)) U R
Complement:
NBW
F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))
Equivalent:
F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r))
Complement:
¬ (F p → ¬ p U (q ∧ ¬ p ∧ X (¬ p U r)))
•
F p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))) W (p ∧ (¬ q ∨ p ∨ X (¬ r W (p ∧ ¬ r))))
NBW
F (p ∧ X F q) → ¬ p U r
Equivalent:
F (p ∧ X F q) → ¬ p U r
Complement:
¬ (F (p ∧ X F q) → ¬ p U r)
•
F (p ∧ X F q) ∧ ¬ r W (p ∧ ¬ r)
NBW
F (p ∧ X F q) ∧ ¬ r W (p ∧ ¬ r)
Equivalent:
¬ (F (p ∧ X F q) → ¬ p U r)
•
F (p ∧ X F q) ∧ ¬ r W (p ∧ ¬ r)
Complement:
F (p ∧ X F q) → ¬ p U r
NBW
G F (q ∧ Y (¬ q S p))
Equivalent:
G F (q ∧ Y (¬ q S p))
•
G F p ∧ G F q
Complement:
¬ (G F p ∧ G F q)
•
F G (¬ q ∨ Z (¬ p B (q ∧ ¬ p)))
•
F G ¬ p ∨ F G ¬ q
•
¬ G F (q ∧ Y (¬ q S p))
DBW
G F (¬ q ∧ Z ((¬ p ∨ q) B (¬ p ∧ (¬ p ∨ q))))
Equivalent:
¬ (F G p ∨ F G q)
•
¬ F G (q ∨ Y (p S (p ∧ ¬ q)))
•
G F (¬ q ∧ Z ((¬ p ∨ q) B (¬ p ∧ (¬ p ∨ q))))
•
G F ¬ p ∧ G F ¬ q
Complement:
F G (q ∨ Y (p S (p ∧ ¬ q)))
•
F G p ∨ F G q
NBW
F G (q ∨ Y (p S (p ∧ ¬ q)))
Equivalent:
F G (q ∨ Y (p S (p ∧ ¬ q)))
•
F G p ∨ F G q
Complement:
¬ (F G p ∨ F G q)
•
¬ F G (q ∨ Y (p S (p ∧ ¬ q)))
•
G F (¬ q ∧ Z ((¬ p ∨ q) B (¬ p ∧ (¬ p ∨ q))))
•
G F ¬ p ∧ G F ¬ q
NBW
¬ (G F p ∧ G F q)
Equivalent:
¬ (G F p ∧ G F q)
•
F G (¬ q ∨ Z (¬ p B (q ∧ ¬ p)))
•
F G ¬ p ∨ F G ¬ q
•
¬ G F (q ∧ Y (¬ q S p))
Complement:
G F (q ∧ Y (¬ q S p))
•
G F p ∧ G F q
NBW
