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
1
2
3
[4]
5
6
7
8
9
Next >
Last page >>
46 - 60 / 392; page
/ 27
p ∧ G ¬ q
Equivalent:
¬ (p → F q)
•
p ∧ G ¬ q
•
¬ F (O (Z False ∧ p) → q)
•
G (O (Z False ∧ p) ∧ ¬ q)
Complement:
p → F q
•
F (O (Z False ∧ p) → q)
NBW
¬ (¬ p U ¬ q)
Equivalent:
¬ (¬ p U ¬ q)
•
p R q
•
q W (p ∧ q)
•
q ∧ p ∨ q ∧ X (p R q)
Complement:
¬ (p R q)
•
¬ p U ¬ q
•
(¬ q ∨ ¬ p) ∧ (¬ q ∨ X (¬ p U ¬ q))
•
¬ (q ∧ p ∨ q ∧ X (p R q))
NBW
p W (q ∨ r)
Equivalent:
p W (q ∨ r)
•
p W q ∨ p W r
Complement:
(¬ q ∧ ¬ r) U (¬ p ∧ ¬ q ∧ ¬ r)
•
¬ (p W (q ∨ r))
•
¬ (p W q ∨ p W r)
•
¬ q U (¬ p ∧ ¬ q) ∧ ¬ r U (¬ p ∧ ¬ r)
NBW
¬ ((p ∧ q) U r)
Equivalent:
¬ ((p ∧ q) U r)
•
¬ (p ∧ q) R ¬ r
•
¬ r W ((¬ p ∨ ¬ q) ∧ ¬ r)
•
¬ (p U r ∧ q U r)
•
¬ r W (¬ p ∧ ¬ r) ∨ ¬ r W (¬ q ∧ ¬ r)
Complement:
(p ∧ q) U r
•
p U r ∧ q U r
NBW
¬ p W (¬ p ∧ q)
Equivalent:
¬ p W (¬ p ∧ q)
Complement:
¬ (¬ p W (¬ p ∧ q))
•
(p ∨ ¬ q) U (p ∧ (p ∨ ¬ q))
NBW
¬ p W q
Equivalent:
¬ p W q
•
G (p → O q)
Complement:
¬ (¬ p W q)
•
¬ q U (p ∧ ¬ q)
•
F (p ∧ H ¬ q)
•
¬ G (p → O q)
NBW
¬ q W p
Equivalent:
¬ q W p
•
G (q → O p)
Complement:
¬ (¬ q W p)
•
¬ p U (q ∧ ¬ p)
•
F (q ∧ H ¬ p)
•
¬ G (q → O p)
NBW
(p ∧ q) U r
Equivalent:
(p ∧ q) U r
•
p U r ∧ q U r
Complement:
¬ ((p ∧ q) U r)
•
¬ (p ∧ q) R ¬ r
•
¬ r W ((¬ p ∨ ¬ q) ∧ ¬ r)
•
¬ (p U r ∧ q U r)
•
¬ r W (¬ p ∧ ¬ r) ∨ ¬ r W (¬ q ∧ ¬ r)
NBW
(p ∨ q) U (q ∧ (p ∨ q))
Equivalent:
(p ∨ q) U (q ∧ (p ∨ q))
•
¬ (¬ p R ¬ q)
•
¬ (¬ q W (¬ p ∧ ¬ q))
•
p U q
•
(p U q) U q
•
(p U q) W q
•
(p W q) U q
•
p U q U q
•
p U p U q
•
p W q ∧ F q
•
q ∨ p ∧ X (p U q)
•
F (q ∧ Z H p)
Complement:
¬ (p U q)
•
¬ p R ¬ q
•
¬ q W (¬ p ∧ ¬ q)
•
¬ ((p U q) U q)
•
¬ ((p U q) W q)
•
¬ ((p W q) U q)
•
¬ (p U p U q)
•
¬ (p U q) R ¬ q
•
¬ (p W q ∧ F q)
•
¬ (p W q) R ¬ q
•
¬ (q ∨ p ∧ X (p U q))
•
¬ p R ¬ (p U q)
•
¬ q ∧ (¬ p ∨ X (¬ q W (¬ p ∧ ¬ q)))
•
¬ q U (¬ p ∧ ¬ q) ∨ G ¬ q
•
¬ q U (¬ q W (¬ p ∧ ¬ q) ∧ ¬ q)
•
¬ q W (¬ q U (¬ p ∧ ¬ q) ∧ ¬ q)
•
¬ q W (¬ q W (¬ p ∧ ¬ q) ∧ ¬ q)
•
(¬ q W (¬ p ∧ ¬ q)) W (¬ p ∧ ¬ q W (¬ p ∧ ¬ q))
•
¬ F (q ∧ Z H p)
•
G (¬ q ∨ Y O ¬ p)
NBW
(p ∨ ¬ q) U (¬ q ∧ (p ∨ ¬ q))
Equivalent:
(p ∨ ¬ q) U (¬ q ∧ (p ∨ ¬ q))
•
¬ (q W (¬ p ∧ q))
•
p U ¬ q
•
F (Z H p ∧ ¬ q)
•
¬ G (Z H p → q)
•
F (Z H p ∧ O ¬ q)
•
¬ G (Z H p → H q)
Complement:
¬ (p U ¬ q)
•
q W (¬ p ∧ q)
•
G (Z H p → q)
•
G (Z H p → H q)
NBW
(¬ q ∧ ¬ r) U (¬ p ∧ ¬ q ∧ ¬ r)
Equivalent:
(¬ q ∧ ¬ r) U (¬ p ∧ ¬ q ∧ ¬ r)
•
¬ (p W (q ∨ r))
•
¬ (p W q ∨ p W r)
•
¬ q U (¬ p ∧ ¬ q) ∧ ¬ r U (¬ p ∧ ¬ r)
Complement:
p W (q ∨ r)
•
p W q ∨ p W r
NBW
¬ q U (¬ p ∧ ¬ q)
Equivalent:
¬ (p W q)
•
¬ q U (¬ p ∧ ¬ q)
•
¬ ((p W q) W q)
•
¬ (p U p W q)
•
¬ (p U q ∨ G p)
•
¬ (p W p U q)
•
¬ (p W p W q)
•
¬ (q ∨ p ∧ X (p W q))
•
¬ p R ¬ (p W q)
•
¬ q ∧ (¬ p ∨ X (¬ q U (¬ p ∧ ¬ q)))
•
¬ q U (¬ q U (¬ p ∧ ¬ q) ∧ ¬ q)
•
¬ q W (¬ p ∧ ¬ q) ∧ F ¬ p
•
(¬ q U (¬ p ∧ ¬ q)) U (¬ p ∧ ¬ q U (¬ p ∧ ¬ q))
•
(¬ q U (¬ p ∧ ¬ q)) W (¬ p ∧ ¬ q U (¬ p ∧ ¬ q))
•
(¬ q W (¬ p ∧ ¬ q)) U (¬ p ∧ ¬ q W (¬ p ∧ ¬ q))
•
F (O ¬ p ∧ H ¬ q)
•
¬ G (O ¬ p → O q)
Complement:
(p ∨ q) W (q ∧ (p ∨ q))
•
¬ (¬ q U (¬ p ∧ ¬ q))
•
q R ¬ (¬ p ∧ ¬ q)
•
p W q
•
(p W q) W q
•
G (¬ p → O q)
•
p U p W q
•
p U q ∨ G p
•
p W p U q
•
p W p W q
•
q ∨ p ∧ X (p W q)
•
G (O ¬ p → O q)
NBW
¬ p U ¬ q
Equivalent:
¬ (p R q)
•
¬ p U ¬ q
•
(¬ q ∨ ¬ p) ∧ (¬ q ∨ X (¬ p U ¬ q))
•
¬ (q ∧ p ∨ q ∧ X (p R q))
Complement:
¬ (¬ p U ¬ q)
•
p R q
•
q W (p ∧ q)
•
q ∧ p ∨ q ∧ X (p R q)
NBW
¬ G ¬ p
Equivalent:
F p
•
True U p
•
¬ G ¬ p
•
O F p
•
F (True S p)
•
F O p
•
F F p
•
p ∨ X F p
•
F G O p
•
G (F p ∨ O p)
•
G F O p
Complement:
¬ (True U p)
•
¬ F p
•
False R ¬ p
•
¬ p W (False ∧ ¬ p)
•
G ¬ p
•
¬ (p ∨ X F p)
•
¬ O F p
•
¬ F (True S p)
•
¬ F O p
•
¬ F F p
•
H G ¬ p
•
¬ p ∧ X G ¬ p
•
G (¬ p B (False ∧ ¬ p))
•
G H ¬ p
•
G G ¬ p
•
F (G ¬ p ∧ H ¬ p)
•
F G H ¬ p
•
¬ F G O p
•
¬ G (F p ∨ O p)
•
¬ G F O p
•
G F H ¬ p
DBW
¬ G p
Equivalent:
¬ (False R p)
•
¬ (p W False)
•
F ¬ p
•
True U (¬ p ∧ True)
•
True U ¬ p
•
p U ¬ p
•
¬ G p
•
¬ (p ∧ X G p)
•
F (True S (¬ p ∧ True))
•
F F ¬ p
•
¬ G (p B False)
•
¬ G G p
•
¬ p ∨ X F ¬ p
•
F G O ¬ p
•
¬ F G H p
•
¬ G F H p
•
G F O ¬ p
Complement:
¬ F ¬ p
•
False R p
•
G p
•
p W False
•
G (p B False)
•
G G p
•
p ∧ X G p
•
F G H p
•
G F H p
DBW