ماشین بوخی توسعه یافته یک نوع دیگر از ماشین بوخی در نظریه آتوماتا می باشد. تفاوت آن با ماشین بوخی شرایط پذیرش آن می باشد که در اینجا یک مجموعه از مجموعه های حالت است. یک چرخهٔ اجرا توسط این ماشین پذیرفته می شود اگر آن حداقل یک حالت از هر مجموعه از شرط پذیرش را که اغلب نامحدود است، ببیند. ماشین بوخی توسعه یافته در قدرت بیان با ماشین بوخی هم ارز است.در وارسی صوری، روش چک کردن مدل نیاز دارد تا یک ماشین را از یک فرمول LTL (منطق زمانی خطی) به گونه ای بدست اورد که ویژگی های برنامه را مشخص کند. الگوریتم هایی وجود دارند که یک فرمول LTL را به یک ماشین بوخی توسعه یافته برای این منظور، تبدیل می کنند. به ویژه نماد GBA (ماشین بوخی توسعه یافته) برای این تبدیل مطرح شد.
φ یک مجموعهٔ متناهی است. مولفه های φ را حالتهای A می نامند.
Σ یک مجموعهٔ متناهی است که آنرا الفبای A می نامند.
Δ : ϕ ∗ Σ → 2 ϕ {\displaystyle \Delta :\phi *\Sigma \rightarrow 2^{\phi }} یک تابع است که آنرا رابطه انتقال A می نامند.
ϕ 0 {\displaystyle \phi _{0}} یک زیرمجموعه از φ است که حالتهای اولیه نامیده می شود.
F 1 , . . . , F n {\displaystyle {F_{1},...,F_{n}}} که برای هر 1 ≤ i ≤ n {\displaystyle 1\leq i\leq n} داریم F i ⊆ ϕ {\displaystyle F_{i}\subseteq \phi } ، شرط پذیرش است.
به طور رسمی یک ماشین بوخی توسعه یافته یک چند تایی A = ( ϕ , Σ , Δ , ϕ 0 , { F 1 , . . . , F n } ) {\displaystyle A=(\phi ,\Sigma ,\Delta ,\phi _{0},\left\{F_{1},...,F_{n}\right\})} است که شامل اجزاء زیر است:
A دقیقاً آن چرخه های اجرا را می پذیرد که در آن مجموعه حالتهای اتفاق افتاده که اغلب نامحدود است، شامل حداقل یک حالت از هر { F 1 , . . . , F n } {\displaystyle \left\{F_{1},...,F_{n}\right\}} باشد.برای توضیح جامع تر ماشینωرا ببینید.
ماشین بوخی توسعه یافته برچسب دار(LGBA)یک گونهٔ دیگر است که در آن ورودی به عنوان برچسب هایی با حالات به جای برچسب های با انتقال ها، همراه است. ماشین بوخی توسعه یافته برچسب دارتوسط گرس و همکارانش معرفی شد.به طور رسمی، یک ماشین بوخی توسعه یافته برچسب دار یک چند تایی A = ( ϕ , Σ , L , Δ , ϕ 0 , { F 1 , . . . , F n } ) {\displaystyle A=(\phi ,\Sigma ,L,\Delta ,\phi _{0},\left\{F_{1},...,F_{n}\right\})} است که شامل اجزاء زیر است:
φ یک مجموعهٔ متناهی است. مولفه های φ را حالتهای A می نامند.
Σ یک مجموعهٔ متناهی است که آنرا الفبای A می نامند.
Δ : ϕ ∗ Σ → 2 ϕ {\displaystyle \Delta :\phi *\Sigma \rightarrow 2^{\phi }} یک تابع است که آنرا رابطه انتقال A می نامند.
ϕ 0 {\displaystyle \phi _{0}} یک زیرمجموعه از φ است که حالتهای اولیه نامیده می شود.
F 1 , . . . , F n {\displaystyle {F_{1},...,F_{n}}} که برای هر 1 ≤ i ≤ n {\displaystyle 1\leq i\leq n} داریم F i ⊆ ϕ {\displaystyle F_{i}\subseteq \phi } ، شرط پذیرش است.
به طور رسمی یک ماشین بوخی توسعه یافته یک چند تایی A = ( ϕ , Σ , Δ , ϕ 0 , { F 1 , . . . , F n } ) {\displaystyle A=(\phi ,\Sigma ,\Delta ,\phi _{0},\left\{F_{1},...,F_{n}\right\})} است که شامل اجزاء زیر است:
A دقیقاً آن چرخه های اجرا را می پذیرد که در آن مجموعه حالتهای اتفاق افتاده که اغلب نامحدود است، شامل حداقل یک حالت از هر { F 1 , . . . , F n } {\displaystyle \left\{F_{1},...,F_{n}\right\}} باشد.برای توضیح جامع تر ماشینωرا ببینید.
ماشین بوخی توسعه یافته برچسب دار(LGBA)یک گونهٔ دیگر است که در آن ورودی به عنوان برچسب هایی با حالات به جای برچسب های با انتقال ها، همراه است. ماشین بوخی توسعه یافته برچسب دارتوسط گرس و همکارانش معرفی شد.به طور رسمی، یک ماشین بوخی توسعه یافته برچسب دار یک چند تایی A = ( ϕ , Σ , L , Δ , ϕ 0 , { F 1 , . . . , F n } ) {\displaystyle A=(\phi ,\Sigma ,L,\Delta ,\phi _{0},\left\{F_{1},...,F_{n}\right\})} است که شامل اجزاء زیر است:
wiki: ماشین بوخی توسعه یافته