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
17
18
19
20
21
[22]
23
24
25
26
27
Next >
Last page >>
316 - 330 / 395; page
/ 27
X X X p
Equivalent:
X X X p
Complement:
NBW
X X F p
Equivalent:
X X F p
Complement:
DBW
F (p ∧ q) ∨ G F p
Equivalent:
F (p ∧ q) ∨ G F p
Complement:
NBW
(G p → G F q) ∧ r
Equivalent:
(G p → G F q) ∧ r
Complement:
NBW
F r → (p → ¬ r U (q ∧ ¬ r)) U r
Equivalent:
F r → (p → ¬ r U (q ∧ ¬ r)) U r
Complement:
¬ (F r → (p → ¬ r U (q ∧ ¬ r)) U r)
NBW
G ¬ q ∨ F (q ∧ F p)
Equivalent:
G ¬ q ∨ F (q ∧ F p)
Complement:
¬ (G ¬ q ∨ F (q ∧ F p))
NBW
G (p → F (q ∧ F r))
Equivalent:
G (p → F (q ∧ F r))
Complement:
F (p ∧ G (¬ q ∨ G ¬ r))
•
¬ G (p → F (q ∧ F r))
DBW
F ¬ p ∨ F (p ∧ ¬ q W r)
Equivalent:
F ¬ p ∨ F (p ∧ ¬ q W r)
Complement:
G p ∧ G (¬ p ∨ ¬ r U (q ∧ ¬ r))
•
¬ (F ¬ p ∨ F (p ∧ ¬ q W r))
NBW
G ¬ r ∨ F (r ∧ ¬ p W q)
Equivalent:
G ¬ r ∨ F (r ∧ ¬ p W q)
Complement:
¬ (G ¬ r ∨ F (r ∧ ¬ p W q))
NBW
G (p → F (q ∧ ¬ r ∧ X (¬ r U s)))
Equivalent:
G (p → F (q ∧ ¬ s ∧ X (¬ s U r)))
•
G (p → F (q ∧ ¬ r ∧ X (¬ r U s)))
Complement:
¬ G (p → F (q ∧ ¬ r ∧ X (¬ r U s)))
•
F (p ∧ G (¬ q ∨ r ∨ X (¬ s W (r ∧ ¬ s))))
NBW
G F ¬ a ∨ G F b
Equivalent:
G F ¬ a ∨ G F b
Complement:
NBW
F X X X p
Equivalent:
F X X X p
Complement:
NBW
G (DESTINO → X (MOSTRAR U (INGRESO ∧ X (ERROR ∨ OK))))
Equivalent:
G (DESTINO → X (MOSTRAR U (INGRESO ∧ X (ERROR ∨ OK))))
Complement:
NBW
G p → X (X q ∨ X r)
Equivalent:
G p → X (X q ∨ X r)
Complement:
NBW
F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))
Equivalent:
F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s))
Complement:
¬ (F p → ¬ q U (p ∨ r ∧ ¬ q ∧ X (¬ q U s)))
•
F p ∧ (¬ p ∧ (¬ r ∨ q ∨ X (¬ s W (q ∧ ¬ s)))) W (q ∧ ¬ p ∧ (¬ r ∨ q ∨ X (¬ s W (q ∧ ¬ s))))
NBW