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
5
6
7
8
9
[10]
11
12
13
14
15
Next >
Last page >>
136 - 150 / 378; page
/ 26
G F (p U (p ∧ q))
Equivalent:
G F (p U (p ∧ q))
Complement:
DBW
G F (p → F q)
Equivalent:
G F (p → F q)
Complement:
DBW
∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (p → t)
Equivalent:
∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (p → t)
Complement:
¬ (∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (p → t))
•
∀ t : ¬ t ∨ F (t ∧ X t ∨ X ¬ t ∧ ¬ t) ∨ F (p ∧ ¬ t)
NBW
G F (¬ p U q)
Equivalent:
G F (¬ p U q)
Complement:
F G (¬ q W (p ∧ ¬ q))
•
¬ G F (¬ p U q)
NBW
G p ∧ G (¬ p ∨ ¬ r U (q ∧ ¬ r))
Equivalent:
G p ∧ G (¬ p ∨ ¬ r U (q ∧ ¬ r))
•
¬ (F ¬ p ∨ F (p ∧ ¬ q W r))
Complement:
F ¬ p ∨ F (p ∧ ¬ q W r)
NBW
¬ G F (¬ p U q)
Equivalent:
F G (¬ q W (p ∧ ¬ q))
•
¬ G F (¬ p U q)
Complement:
G F (¬ p U q)
NBW
F G p → G F q
Equivalent:
¬ F G p ∨ G F q
•
F G p → G F q
Complement:
¬ (F G p → G F q)
•
F G p ∧ F G ¬ q
NBW
F G p ∧ F G ¬ q
Equivalent:
¬ (F G p → G F q)
•
F G p ∧ F G ¬ q
Complement:
¬ F G p ∨ G F q
•
F G p → G F q
NBW
G (G F p → F q)
Equivalent:
G (G F p → F q)
•
G F p → G F q
•
G F q ∨ F G ¬ p
Complement:
¬ (G F p → G F q)
•
¬ (G F q ∨ F G ¬ p)
•
F (G F p ∧ G ¬ q)
•
F G ¬ q ∧ G F p
•
¬ G (G F p → F q)
•
G F p ∧ F G ¬ q
NBW
G F p ∨ F G q
Equivalent:
G F p ∨ F G q
Complement:
¬ (G F p ∨ F G q)
•
F G ¬ p ∧ G F ¬ q
NBW
p → G (p ∧ q)
Equivalent:
p → G (p ∧ q)
Complement:
NBW
p → F (p ∧ q)
Equivalent:
p → F (p ∧ q)
Complement:
DBW
p → X q
Equivalent:
p → X q
Complement:
NBW
X p → Gq
Equivalent:
X p → Gq
Complement:
NBW
G ¬ p ∨ Fq
Equivalent:
G ¬ p ∨ Fq
Complement:
NBW