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
19
20
21
22
23
[24]
25
26
27
Next >
Last page >>
346 - 360 / 395; page
/ 27
F G p ∨ F G q ∨ F G r ∨ F G s
Equivalent:
F G p ∨ F G q ∨ F G r ∨ F G s
Complement:
NBW
¬ G (s → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U (t ∨ G (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p)))))
Equivalent:
¬ G (s → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U (t ∨ G (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p)))))
Complement:
G (s → (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p))) U (t ∨ G (q ∧ X (¬ t U r) → X (¬ t U (r ∧ F p)))))
NBW
F p R F q
Equivalent:
F p R F q
Complement:
NBW
F P → ¬ P U (S ∧ ¬ P ∧ ¬ P U T)
Equivalent:
F P → ¬ P U (S ∧ ¬ P ∧ ¬ P U T)
Complement:
NBW
X X X X p
Equivalent:
X X X X p
Complement:
NBW
X X (a ∨ F G b)
Equivalent:
X X (a ∨ F G b)
Complement:
NBW
F s → ¬ (q ∧ ¬ s ∧ X (¬ s U (r ∧ ¬ s))) U (s ∨ p)
Equivalent:
F s → ¬ (q ∧ ¬ s ∧ X (¬ s U (r ∧ ¬ s))) U (s ∨ p)
Complement:
¬ (F s → ¬ (q ∧ ¬ s ∧ X (¬ s U (r ∧ ¬ s))) U (s ∨ p))
NBW
G (s ∧ F t → ¬ (q ∧ ¬ t ∧ X (¬ t U (r ∧ ¬ t))) U (t ∨ p))
Equivalent:
G (s ∧ F t → ¬ (q ∧ ¬ t ∧ X (¬ t U (r ∧ ¬ t))) U (t ∨ p))
Complement:
¬ G (s ∧ F t → ¬ (q ∧ ¬ t ∧ X (¬ t U (r ∧ ¬ t))) U (t ∨ p))
NBW
F s → (p → ¬ s U (q ∧ ¬ s ∧ X (¬ s U r))) U s
Equivalent:
F s → (p → ¬ s U (q ∧ ¬ s ∧ X (¬ s U r))) U s
Complement:
¬ (F s → (p → ¬ s U (q ∧ ¬ s ∧ X (¬ s U r))) U s)
NBW
F t → (p → ¬ t U (q ∧ ¬ t ∧ ¬ s ∧ X ((¬ t ∧ ¬ s) U r))) U t
Equivalent:
F t → (p → ¬ t U (q ∧ ¬ t ∧ ¬ s ∧ X ((¬ t ∧ ¬ s) U r))) U t
Complement:
¬ (F t → (p → ¬ t U (q ∧ ¬ t ∧ ¬ s ∧ X ((¬ t ∧ ¬ s) U r))) U t)
NBW
¬ (¬ p W p W ¬ p W p W G ¬ p)
Equivalent:
¬ (¬ p W p W ¬ p W p W G ¬ p)
•
(((F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))) U (¬ p ∧ (F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p)))) U (p ∧ ((F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))) U (¬ p ∧ (F p U (¬ p ∧ F p)) U (p ∧ F p U (¬ p ∧ F p))))
Complement:
¬ p W p W ¬ p W p W G ¬ p
NBW
F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q)
Equivalent:
F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q)
Complement:
¬ (F p → ¬ p U (p ∧ ¬ q W q W ¬ q W q W G ¬ q))
•
F p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))) W (p ∧ (¬ p ∨ (((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q)))) U (q ∧ ((F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))) U (¬ q ∧ (F q U (¬ q ∧ F q)) U (q ∧ F q U (¬ q ∧ F q))))))
NBW
G F p ∧ G F q ∧ G F r ∧ G F s ∧ G F t
Equivalent:
G F p ∧ G F q ∧ G F r ∧ G F s ∧ G F t
Complement:
DBW
F G p ∨ F G q ∨ F G r ∨ F G s ∨ F G t
Equivalent:
F G p ∨ F G q ∨ F G r ∨ F G s ∨ F G t
Complement:
NBW
G (S ∧ F T → F (T ∧ F P))
Equivalent:
G (S ∧ F T → F (T ∧ F P))
Complement:
NBW
