ماشین بوخی توسعه یافته

به طور رسمی یک ماشین بوخی توسعه یافته یک چند تایی${\displaystyle A=(\varphi ,\mathrm{\Sigma },\mathrm{\Delta },{\varphi }_0,\left\{F_1,...,F_n\right\})}$

• φ یک مجموعهٔ متناهی است. مولفه‌های φ را حالتهای A می‌نامند.
• Σ یک مجموعهٔ متناهی است که آنرا الفبای A می‌نامند.
• ${\displaystyle \mathrm{\Delta }:\varphi \ast \mathrm{\Sigma }\to 2^{\varphi }}$
  یک تابع است که آنرا رابطه انتقال A می‌نامند.
• ${\displaystyle {\varphi }_0}$
  یک زیرمجموعه از φ است که حالتهای اولیه نامیده می‌شود.
• ${\displaystyle F_1,...,F_n}$
  که برای هر ${\displaystyle 1\le i\le n}$
  داریم ${\displaystyle F_i\subseteq \varphi }$
  ، شرط پذیرش است.

A دقیقاً آن چرخه‌های اجرا را می‌پذیرد که در آن مجموعه حالتهای اتفاق افتاده که اغلب نامحدود است، شامل حداقل یک حالت از هر${\displaystyle \left\{F_1,...,F_n\right\}}$

ماشین بوخی توسعه یافته برچسب دار(LGBA)یک گونهٔ دیگر است که در آن ورودی به عنوان برچسب‌هایی با حالات به جای برچسب‌های با انتقال‌ها، همراه است. ماشین بوخی توسعه یافته برچسب دارتوسط گرس و همکارانش معرفی شد. به طور رسمی، یک ماشین بوخی توسعه یافته برچسب دار یک چند تایی${\displaystyle A=(\varphi ,\mathrm{\Sigma },L,\mathrm{\Delta },{\varphi }_0,\left\{F_1,...,F_n\right\})}$

• φ یک مجموعهٔ متناهی است. مولفه‌های φ را حالتهای A می‌نامند.
• Σ یک مجموعهٔ متناهی است که آنرا الفبای A می‌نامند.
• ${\displaystyle L:\varphi \to 2^{\mathrm{\Sigma }}}$
  یک تابع است که آنرا تابع برچسب A می‌نامند.
• ${\displaystyle \mathrm{\Delta }:\varphi \ast \mathrm{\Sigma }\to 2^{\varphi }}$
  یک تابع است که آنرا رابطه انتقال A می‌نامند.
• ${\displaystyle {\varphi }_0}$
  یک زیرمجموعه از φ است که حالتهای اولیه نامیده می‌شود.
• ${\displaystyle \left\{F_1,...,F_n\right\}}$
  که برای هر ${\displaystyle 1\le i\le n}$
  داریم ${\displaystyle F_i\subseteq \varphi }$
  ، شرط پذیرش است.

فرض کنید${\displaystyle w=a_1{a}_2...}$

A دقیقاً آن چرخه‌های اجرایی را می‌پذیرد که در آن مجموعه حالتهای اتفاق افتاده که اغلب نامحدود است، شامل حداقل یک حالت از هر ${\displaystyle F_1,...,F_n}$

برای بدست آوردن مدل غیر برچسب دار آن، برچسب‌ها از گره‌ها به انتقالات واردشده حذف می‌شوند.

ماشین بوخی توسعه یافته

• "Generalized Büchi automaton" (به انگلیسی).