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 / 395; page
/ 27
(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
¬ (F p → ¬ q U (r ∨ p))
Equivalent:
F p ∧ (¬ r ∧ ¬ p) W (q ∧ ¬ r ∧ ¬ p)
•
¬ (F p → ¬ q U (r ∨ p))
Complement:
F p → ¬ q U (r ∨ p)
NBW
X F p
Equivalent:
X F p
Complement:
X G ¬ p
NBW
X F ¬ p
Equivalent:
X F ¬ p
Complement:
X G p
NBW
G p ∨ F q
Equivalent:
G p ∨ F q
•
p W F q
Complement:
¬ (G p ∨ F q)
•
¬ (p W F q)
•
F ¬ p ∧ G ¬ q
•
G ¬ q U (¬ p ∧ G ¬ q)
NBW
G ¬ p ∨ F ¬ q
Equivalent:
¬ (F p ∧ G q)
•
G ¬ p ∨ F ¬ q
Complement:
F p ∧ G q
NBW
¬ G (F p ∧ q)
Equivalent:
F (G ¬ p ∨ ¬ q)
•
¬ G (F p ∧ q)
Complement:
G (F p ∧ q)
NBW