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
2
3
4
5
6
[7]
8
9
10
11
12
Next >
Last page >>
91 - 105 / 392; page
/ 27
G (p → X (q ∧ r))
Equivalent:
G (p → X (q ∧ r))
Complement:
NBW
G (p → X (q ∧ ¬ r) ∨ ¬ q ∧ r)
Equivalent:
G (p → X (q ∧ ¬ r) ∨ ¬ q ∧ r)
Complement:
NBW
G (p → X (q ∧ ¬ r))
Equivalent:
G (p → X (q ∧ ¬ r))
Complement:
NBW
G (p U (q ∧ ¬ p))
Equivalent:
G (p U (q ∧ ¬ p))
Complement:
NBW
G (p → G (q → Fr))
Equivalent:
G (p → G (q → Fr))
Complement:
NBW
G (p → ¬ R W (P ∧ ¬ R))
Equivalent:
G (p → ¬ R W (P ∧ ¬ R))
Complement:
NBW
G (p → q → F r)
Equivalent:
G (p → q → F r)
Complement:
DBW
G ((¬ p1 ∧ ¬ p2) ∧ t1 ∧ t2) → F (p1 ∨ p2)
Equivalent:
G ((¬ p1 ∧ ¬ p2) ∧ t1 ∧ t2) → F (p1 ∨ p2)
Complement:
DBW
G (p → X p)
Equivalent:
G (p → X p)
•
G (p → G p)
Complement:
F (p ∧ X ¬ p)
•
F (p ∧ F ¬ p)
•
¬ G (p → X p)
•
¬ G (p → G p)
NBW
G (p ∧ ¬ q → Z (p ∨ q))
Equivalent:
G (p → p B q)
•
G (p ∧ ¬ q → Z (p ∨ q))
Complement:
F (p ∧ ¬ q ∧ Y (¬ p ∧ ¬ q))
•
F (p ∧ ¬ q S (¬ p ∧ ¬ q))
•
¬ G (p → p B q)
•
¬ G (p ∧ ¬ q → Z (p ∨ q))
NBW
G (p → p S q)
Equivalent:
G (p → p S q)
Complement:
F (p ∧ ¬ q B (¬ p ∧ ¬ q))
•
¬ G (p → p S q)
NBW
G (p ∧ ¬ q → X (p ∨ q))
Equivalent:
G (p → p W q)
•
G (p ∧ ¬ q → X (p ∨ q))
Complement:
F (p ∧ ¬ q ∧ X (¬ p ∧ ¬ q))
•
F (p ∧ ¬ q U (¬ p ∧ ¬ q))
•
¬ G (p → p W q)
•
¬ G (p ∧ ¬ q → X (p ∨ q))
NBW
G (p → ¬ q W r)
Equivalent:
G (p → ¬ q W r)
•
G (q → ¬ p B r)
Complement:
F (p ∧ ¬ r U (q ∧ ¬ r))
•
F (q ∧ ¬ r S (p ∧ ¬ r))
•
¬ G (p → ¬ q W r)
•
¬ G (q → ¬ p B r)
NBW
G (p ∨ q S r)
Equivalent:
G (p ∨ q S r)
Complement:
F (¬ p ∧ ¬ r B (¬ q ∧ ¬ r))
•
¬ G (p ∨ q S r)
NBW
G (¬ p ∨ O ¬ q)
Equivalent:
¬ F (p ∧ H q)
•
G (¬ p ∨ O ¬ q)
Complement:
F (p ∧ H q)
NBW