Sorted by


Refresh


Filtered by

Automaton Type

Select / Deselect All














State Size

Select / Deselect All






Formula Length

Select / Deselect All






Temporal Hierarchy

Select / Deselect All








Spec Patterns

Select / Deselect All











Refresh


Grouped By


Refresh

False Equivalent: False Y p Y ¬ p ¬ Z p ¬ Z ¬ p Y p ∧ Z False Z p ∧ Y True ¬ G (q → O p) ∧ p ¬ G (p → q U p)
Complement: True ¬ Y p ¬ Y ¬ p Z p Z ¬ p ¬ (Y p ∧ Z False) F p → F p Y ¬ p ∨ Z False ¬ (Z p ∧ Y True) Z ¬ p ∨ Y True Z Z p G (p → F (q → p)) G (p → q U p)
NBW
True Equivalent: True ¬ Y p ¬ Y ¬ p Z p Z ¬ p ¬ (Y p ∧ Z False) F p → F p Y ¬ p ∨ Z False ¬ (Z p ∧ Y True) Z ¬ p ∨ Y True Z Z p G (p → F (q → p)) G (p → q U p)
Complement: False Y p Y ¬ p ¬ Z p ¬ Z ¬ p Y p ∧ Z False Z p ∧ Y True ¬ G (q → O p) ∧ p ¬ G (p → q U p)
NBW
G (p ∨ q) Equivalent: G (p ∨ q) G (p W (q ∧ ¬ p)) G (p W q)
Complement:
NBW
¬ F (p → Fq) Equivalent: ¬ F (p → Fq)
Complement:
NBW
G (p ∨ ¬ q) Equivalent: G (p ∨ ¬ q)
Complement:
NBW
p → F p Equivalent: p → F p
Complement:
DBW
G (¬ p ∧ q) Equivalent: G (¬ p ∧ q)
Complement:
NBW
G (¬ p ∨ q ∧ r) Equivalent: G (¬ p ∨ q ∧ r)
Complement:
NBW
G (p → q ∧ ¬ r) Equivalent: G (p → q ∧ ¬ r)
Complement:
NBW
G (¬ p ∨ ¬ q) Equivalent: G (¬ p ∨ ¬ q)
Complement: F (p ∧ q) ¬ G (¬ p ∨ ¬ q)
NBW
G ¬ p Equivalent: ¬ (True U p) ¬ F p False R ¬ p ¬ p W (False ∧ ¬ p) G ¬ p ¬ (p ∨ X F p) ¬ O F p ¬ F (True S p) ¬ F O p ¬ F F p H G ¬ p ¬ p ∧ X G ¬ p G (¬ p B (False ∧ ¬ p)) G H ¬ p G G ¬ p F (G ¬ p ∧ H ¬ p) F G H ¬ p ¬ F G O p ¬ G (F p ∨ O p) ¬ G F O p G F H ¬ p
Complement: F p True U p ¬ G ¬ p O F p F (True S p) F O p F F p p ∨ X F p F G O p G (F p ∨ O p) G F O p
NBW
G (¬ p ∧ ¬ q) Equivalent: ¬ F (p ∨ q) G (¬ p ∧ ¬ q) ¬ (F p ∨ F q) G ¬ p ∧ G ¬ q
Complement: F (p ∨ q) F p ∨ F q
NBW
G p Equivalent: ¬ F ¬ p False R p G p p W False G (p B False) G G p p ∧ X G p F G H p G F H p
Complement: ¬ (False R p) ¬ (p W False) F ¬ p True U (¬ p ∧ True) True U ¬ p p U ¬ p ¬ G p ¬ (p ∧ X G p) F (True S (¬ p ∧ True)) F F ¬ p ¬ G (p B False) ¬ G G p ¬ p ∨ X F ¬ p F G O ¬ p ¬ F G H p ¬ G F H p G F O ¬ p
NBW
G (p ∧ q) Equivalent: G (p ∧ q) G p ∧ G q
Complement: F (¬ p ∨ ¬ q) ¬ G (p ∧ q) ¬ (G p ∧ G q) F ¬ p ∨ F ¬ q
NBW
G (p → ¬ p U q) Equivalent: G (p → ¬ p U q) G (¬ p W q)
Complement:
NBW