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
9
10
11
12
13
[14]
15
16
17
18
19
Next >
Last page >>
196 - 210 / 401; page
/ 27
X p R q
Equivalent:
X p R q
Complement:
NBW
X p U q
Equivalent:
X p U q
Complement:
NBW
G p ∨ G q
Equivalent:
G p ∨ G q
•
G q ∨ G p
•
G (H p ∨ H q)
Complement:
¬ (G p ∨ G q)
•
F ¬ p ∧ F ¬ q
•
F ¬ q ∧ F ¬ p
•
¬ (G q ∨ G p)
•
F (O ¬ p ∧ O ¬ q)
•
¬ G (H p ∨ H q)
NBW
G ¬ p ∨ G ¬ q
Equivalent:
¬ (F p ∧ F q)
•
G ¬ p ∨ G ¬ q
Complement:
F p ∧ F q
NBW
¬ ((p ∨ Z q) U r)
Equivalent:
¬ ((p ∨ Z q) U r)
•
¬ (p ∨ Z q) R ¬ r
•
¬ r W (¬ p ∧ Y ¬ q ∧ ¬ r)
Complement:
(p ∨ Z q) U r
NBW
F p → ¬ q U (r ∨ p)
Equivalent:
F p → ¬ q U (r ∨ p)
Complement:
F p ∧ (¬ r ∧ ¬ p) W (q ∧ ¬ r ∧ ¬ p)
•
¬ (F p → ¬ q U (r ∨ p))
NBW
(p ∨ Y q) U r
Equivalent:
(p ∨ Y q) U r
Complement:
¬ ((p ∨ Y q) U r)
•
¬ (p ∨ Y q) R ¬ r
•
¬ r W (¬ p ∧ Z ¬ q ∧ ¬ r)
NBW
(p ∨ q S r) U s
Equivalent:
(p ∨ q S r) U s
Complement:
¬ ((p ∨ q S r) U s)
•
¬ (p ∨ q S r) R ¬ s
•
¬ s W (¬ p ∧ ¬ r B (¬ q ∧ ¬ r) ∧ ¬ s)
NBW
¬ G (p → G q)
Equivalent:
F (O p ∧ ¬ q)
•
¬ G (O p → q)
•
F (p ∧ F ¬ q)
•
¬ G (p → G q)
Complement:
G (O p → q)
•
G (p → G q)
NBW
¬ G (p → X p)
Equivalent:
F (p ∧ X ¬ p)
•
F (p ∧ F ¬ p)
•
¬ G (p → X p)
•
¬ G (p → G p)
Complement:
G (p → X p)
•
G (p → G p)
NBW
¬ G (q → G ¬ p)
Equivalent:
F (p ∧ O q)
•
¬ G (q → G ¬ p)
Complement:
G (q → G ¬ p)
•
¬ F (p ∧ O q)
•
G (¬ p ∨ H ¬ q)
NBW
¬ G (p ∧ ¬ q → X (p ∨ q))
Equivalent:
F (p ∧ ¬ q ∧ X (¬ p ∧ ¬ q))
•
F (p ∧ ¬ q U (¬ p ∧ ¬ q))
•
¬ G (p → p W q)
•
¬ G (p ∧ ¬ q → X (p ∨ q))
Complement:
G (p → p W q)
•
G (p ∧ ¬ q → X (p ∨ q))
NBW
¬ G (p ∧ ¬ q → Z (p ∨ q))
Equivalent:
F (p ∧ ¬ q ∧ Y (¬ p ∧ ¬ q))
•
F (p ∧ ¬ q S (¬ p ∧ ¬ q))
•
¬ G (p → p B q)
•
¬ G (p ∧ ¬ q → Z (p ∨ q))
Complement:
G (p → p B q)
•
G (p ∧ ¬ q → Z (p ∨ q))
NBW
¬ G (p → ¬ q W r)
Equivalent:
F (p ∧ ¬ r U (q ∧ ¬ r))
•
F (q ∧ ¬ r S (p ∧ ¬ r))
•
¬ G (p → ¬ q W r)
•
¬ G (q → ¬ p B r)
Complement:
G (p → ¬ q W r)
•
G (q → ¬ p B r)
NBW
¬ G (p → q W r)
Equivalent:
F (p ∧ ¬ r U (¬ q ∧ ¬ r))
•
¬ G (p → q W r)
Complement:
G (p → q W r)
NBW