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
Next >
Last page >>
31 - 45 / 392; page
/ 27
(p ∧ q) B r
Equivalent:
(p ∧ q) B r
•
p B r ∧ q B r
Complement:
¬ ((p ∧ q) B r)
•
¬ r S ((¬ p ∨ ¬ q) ∧ ¬ r)
•
¬ (p B r ∧ q B r)
•
¬ r S (¬ p ∧ ¬ r) ∨ ¬ r S (¬ q ∧ ¬ r)
NBW
¬ (¬ q S (¬ p ∧ ¬ q))
Equivalent:
(p ∨ q) B (q ∧ (p ∨ q))
•
¬ (¬ q S (¬ p ∧ ¬ q))
•
p B q
•
(p B q) B q
•
p B p B q
•
p S q ∨ H p
•
q ∨ p ∧ Z (p B q)
Complement:
¬ (p B q)
•
¬ q S (¬ p ∧ ¬ q)
•
¬ ((p B q) B q)
•
¬ (p B p B q)
•
¬ (p S q ∨ H p)
•
¬ (q ∨ p ∧ Z (p B q))
•
¬ q ∧ (¬ p ∨ Y (¬ q S (¬ p ∧ ¬ q)))
•
¬ q B (¬ p ∧ ¬ q) ∧ O ¬ p
•
¬ q S (¬ q S (¬ p ∧ ¬ q) ∧ ¬ q)
•
(¬ q S (¬ p ∧ ¬ q)) S (¬ p ∧ ¬ q S (¬ p ∧ ¬ q))
NBW
(p ∨ q) S (q ∧ (p ∨ q))
Equivalent:
(p ∨ q) S (q ∧ (p ∨ q))
•
¬ (¬ q B (¬ p ∧ ¬ q))
•
p S q
•
(p S q) S q
•
G p S q
•
p B q ∧ O q
•
p S p S q
•
q ∨ p ∧ Y (p S q)
Complement:
¬ (p S q)
•
¬ q B (¬ p ∧ ¬ q)
•
¬ ((p S q) S q)
•
¬ (p B q ∧ O q)
•
¬ (p S p S q)
•
¬ (q ∨ p ∧ Y (p S q))
•
¬ q ∧ (¬ p ∨ Z (¬ q B (¬ p ∧ ¬ q)))
•
¬ q B (¬ q B (¬ p ∧ ¬ q) ∧ ¬ q)
•
¬ q S (¬ p ∧ ¬ q) ∨ H ¬ q
•
(¬ q B (¬ p ∧ ¬ q)) B (¬ p ∧ ¬ q B (¬ p ∧ ¬ q))
NBW
(¬ q ∧ ¬ r) S (¬ p ∧ ¬ q ∧ ¬ r)
Equivalent:
(¬ q ∧ ¬ r) S (¬ p ∧ ¬ q ∧ ¬ r)
•
¬ (p B (q ∨ r))
•
¬ (p B q ∨ p B r)
•
¬ q S (¬ p ∧ ¬ q) ∧ ¬ r S (¬ p ∧ ¬ r)
Complement:
p B (q ∨ r)
•
p B q ∨ p B r
NBW
¬ (p S q)
Equivalent:
¬ (p S q)
•
¬ q B (¬ p ∧ ¬ q)
•
¬ ((p S q) S q)
•
¬ (p B q ∧ O q)
•
¬ (p S p S q)
•
¬ (q ∨ p ∧ Y (p S q))
•
¬ q ∧ (¬ p ∨ Z (¬ q B (¬ p ∧ ¬ q)))
•
¬ q B (¬ q B (¬ p ∧ ¬ q) ∧ ¬ q)
•
¬ q S (¬ p ∧ ¬ q) ∨ H ¬ q
•
(¬ q B (¬ p ∧ ¬ q)) B (¬ p ∧ ¬ q B (¬ p ∧ ¬ q))
Complement:
(p ∨ q) S (q ∧ (p ∨ q))
•
¬ (¬ q B (¬ p ∧ ¬ q))
•
p S q
•
(p S q) S q
•
G p S q
•
p B q ∧ O q
•
p S p S q
•
q ∨ p ∧ Y (p S q)
NBW
¬ q S (¬ p ∧ ¬ q)
Equivalent:
¬ (p B q)
•
¬ q S (¬ p ∧ ¬ q)
•
¬ ((p B q) B q)
•
¬ (p B p B q)
•
¬ (p S q ∨ H p)
•
¬ (q ∨ p ∧ Z (p B q))
•
¬ q ∧ (¬ p ∨ Y (¬ q S (¬ p ∧ ¬ q)))
•
¬ q B (¬ p ∧ ¬ q) ∧ O ¬ p
•
¬ q S (¬ q S (¬ p ∧ ¬ q) ∧ ¬ q)
•
(¬ q S (¬ p ∧ ¬ q)) S (¬ p ∧ ¬ q S (¬ p ∧ ¬ q))
Complement:
(p ∨ q) B (q ∧ (p ∨ q))
•
¬ (¬ q S (¬ p ∧ ¬ q))
•
p B q
•
(p B q) B q
•
p B p B q
•
p S q ∨ H p
•
q ∨ p ∧ Z (p B q)
NBW
H p
Equivalent:
O p
•
¬ O ¬ p
•
¬ H ¬ p
•
True S p
•
H p
•
p B False
•
O O p
•
F (p B False)
•
F H p
•
H H p
•
G (True S p)
•
G O p
•
p ∧ Z H p
•
p ∨ Y O p
Complement:
¬ (True S p)
•
¬ (p B False)
•
O ¬ p
•
¬ O p
•
¬ H p
•
True S (¬ p ∧ True)
•
H ¬ p
•
¬ p B (False ∧ ¬ p)
•
¬ (p ∧ Z H p)
•
O O ¬ p
•
¬ (p ∨ Y O p)
•
F (¬ p B (False ∧ ¬ p))
•
¬ O O p
•
F H ¬ p
•
¬ F (p B False)
•
¬ F H p
•
¬ H H p
•
¬ G (True S p)
•
H H ¬ p
•
G (True S (¬ p ∧ True))
•
¬ G O p
•
¬ p ∧ Z H ¬ p
•
¬ p ∨ Y O ¬ p
•
G O ¬ p
NBW
H ¬ p
Equivalent:
¬ (True S p)
•
¬ (p B False)
•
O ¬ p
•
¬ O p
•
¬ H p
•
True S (¬ p ∧ True)
•
H ¬ p
•
¬ p B (False ∧ ¬ p)
•
¬ (p ∧ Z H p)
•
O O ¬ p
•
¬ (p ∨ Y O p)
•
F (¬ p B (False ∧ ¬ p))
•
¬ O O p
•
F H ¬ p
•
¬ F (p B False)
•
¬ F H p
•
¬ H H p
•
¬ G (True S p)
•
H H ¬ p
•
G (True S (¬ p ∧ True))
•
¬ G O p
•
¬ p ∧ Z H ¬ p
•
¬ p ∨ Y O ¬ p
•
G O ¬ p
Complement:
O p
•
¬ O ¬ p
•
¬ H ¬ p
•
True S p
•
H p
•
p B False
•
O O p
•
F (p B False)
•
F H p
•
H H p
•
G (True S p)
•
G O p
•
p ∧ Z H p
•
p ∨ Y O p
NBW
p B (q ∨ r)
Equivalent:
p B (q ∨ r)
•
p B q ∨ p B r
Complement:
(¬ q ∧ ¬ r) S (¬ p ∧ ¬ q ∧ ¬ r)
•
¬ (p B (q ∨ r))
•
¬ (p B q ∨ p B r)
•
¬ q S (¬ p ∧ ¬ q) ∧ ¬ r S (¬ p ∧ ¬ r)
NBW
¬ r S ((¬ p ∨ ¬ q) ∧ ¬ r)
Equivalent:
¬ ((p ∧ q) B r)
•
¬ r S ((¬ p ∨ ¬ q) ∧ ¬ r)
•
¬ (p B r ∧ q B r)
•
¬ r S (¬ p ∧ ¬ r) ∨ ¬ r S (¬ q ∧ ¬ r)
Complement:
(p ∧ q) B r
•
p B r ∧ q B r
NBW
(p ∧ q) W r
Equivalent:
(p ∧ q) W r
•
p W r ∧ q W r
Complement:
¬ ((p ∧ q) W r)
•
¬ r U ((¬ p ∨ ¬ q) ∧ ¬ r)
•
¬ (p W r ∧ q W r)
•
¬ r U (¬ p ∧ ¬ r) ∨ ¬ r U (¬ q ∧ ¬ r)
NBW
¬ (¬ q U (¬ p ∧ ¬ q))
Equivalent:
(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)
Complement:
¬ (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)
NBW
¬ (p U (q ∨ r))
Equivalent:
(¬ q ∧ ¬ r) W (¬ p ∧ ¬ q ∧ ¬ r)
•
¬ (p U (q ∨ r))
•
¬ p R ¬ (q ∨ r)
•
¬ (p U q ∨ p U r)
•
¬ q W (¬ p ∧ ¬ q) ∧ ¬ r W (¬ p ∧ ¬ r)
Complement:
p U (q ∨ r)
•
p U q ∨ p U r
NBW
¬ (p U q)
Equivalent:
¬ (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)
Complement:
(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)
NBW
¬ (p U ¬ q)
Equivalent:
¬ (p U ¬ q)
•
q W (¬ p ∧ q)
•
G (Z H p → q)
•
G (Z H p → H q)
Complement:
(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)
NBW