Büchi Store

View the filtered language classes in the "Containment Lattice"

<< First page < Pre [1] 2 3 4 5 6 Next > Last page >>

1 - 15 / 401; page / 27

	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

Sorted by

State Size

Formula Length

Temporal Hierarchy

Spec Patterns

Filtered by

Automaton Type

State Size

Formula Length

Temporal Hierarchy

Spec Patterns

Grouped By