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
3
4
5
6
7
[8]
9
10
11
12
13
Next >
Last page >>
106 - 120 / 392; page
/ 27
G (q → G ¬ p)
Equivalent:
G (q → G ¬ p)
•
¬ F (p ∧ O q)
•
G (¬ p ∨ H ¬ q)
Complement:
F (p ∧ O q)
•
¬ G (q → G ¬ p)
NBW
∃ t : G ((t ↔ Z ¬ t) ∧ (t → p))
Equivalent:
∃ t : G ((t ↔ Z ¬ t) ∧ (t → p))
•
∃ t : t ∧ G ((t → p) ∧ (t ↔ X ¬ t))
•
∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (t → p)
Complement:
¬ (∃ t : t ∧ G (t ↔ X ¬ t) ∧ G (t → p))
•
∀ t : ¬ t ∨ F (t ∧ X t ∨ X ¬ t ∧ ¬ t) ∨ F (t ∧ ¬ p)
NBW
G (p → q W r)
Equivalent:
G (p → q W r)
Complement:
F (p ∧ ¬ r U (¬ q ∧ ¬ r))
•
¬ G (p → q W r)
NBW
X G p
Equivalent:
X G p
Complement:
X F ¬ p
NBW
X G ¬ p
Equivalent:
X G ¬ p
Complement:
X F p
NBW
G (q ∧ ¬ r → ¬ p W r)
Equivalent:
G (q ∧ ¬ r → ¬ p W r)
Complement:
¬ G (q ∧ ¬ r → ¬ p W r)
NBW
G (p → G q)
Equivalent:
G (O p → q)
•
G (p → G q)
Complement:
F (O p ∧ ¬ q)
•
¬ G (O p → q)
•
F (p ∧ F ¬ q)
•
¬ G (p → G q)
NBW
G (q ∧ ¬ r → p W r)
Equivalent:
G (q ∧ ¬ r → p W r)
Complement:
¬ G (q ∧ ¬ r → p W r)
NBW
G (q ∧ ¬ r → ¬ r W (p ∧ ¬ r))
Equivalent:
G (q ∧ ¬ r → ¬ r W (p ∧ ¬ r))
Complement:
¬ G (q ∧ ¬ r → ¬ r W (p ∧ ¬ r))
NBW
G (s ∧ ¬ r → ¬ p W (q ∨ r))
Equivalent:
G (s ∧ ¬ r → ¬ p W (q ∨ r))
Complement:
¬ G (s ∧ ¬ r → ¬ p W (q ∨ r))
NBW
F (p ∧ H q)
Equivalent:
F (p ∧ H q)
Complement:
¬ F (p ∧ H q)
•
G (¬ p ∨ O ¬ q)
NBW
F p ∧ G q
Equivalent:
F p ∧ G q
Complement:
¬ (F p ∧ G q)
•
G ¬ p ∨ F ¬ q
NBW
¬ (G p ∨ F q)
Equivalent:
¬ (G p ∨ F q)
•
¬ (p W F q)
•
F ¬ p ∧ G ¬ q
•
G ¬ q U (¬ p ∧ G ¬ q)
Complement:
G p ∨ F q
•
p W F q
NBW
G F p
Equivalent:
G (True U p)
•
G F p
•
F G F p
Complement:
F (¬ p W (False ∧ ¬ p))
•
F G ¬ p
•
¬ G (True U p)
•
¬ G F p
•
¬ F G F p
•
G F G ¬ p
NBW
G F ¬ p
Equivalent:
¬ F (False R p)
•
¬ F (p W False)
•
¬ F G p
•
G (True U (¬ p ∧ True))
•
G (True U ¬ p)
•
G F ¬ p
•
F G F ¬ p
•
¬ G F G p
Complement:
F (False R p)
•
F (p W False)
•
F G p
•
G F G p
NBW