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

ماشین بوخی توسعه یافته یک نوع دیگر از ماشین بوخی در نظریه آتوماتا می‌باشد. تفاوت آن با ماشین بوخی شرایط پذیرش آن می‌باشد که در اینجا یک مجموعه از مجموعه‌های حالت است. یک چرخهٔ اجرا توسط این ماشین پذیرفته می‌شود اگر آن حداقل یک حالت از هر مجموعه از شرط پذیرش را که اغلب نامحدود است، ببیند. ماشین بوخی توسعه یافته در قدرت بیان با ماشین بوخی هم ارز است. در وارسی صوری، روش چک کردن مدل نیاز دارد تا یک ماشین را از یک فرمول LTL (منطق زمانی خطی) به گونه‌ای بدست اورد که ویژگی‌های برنامه را مشخص کند. الگوریتم‌هایی وجود دارند که یک فرمول LTL را به یک ماشین بوخی توسعه یافته برای این منظور، تبدیل می‌کنند. به ویژه نماد GBA (ماشین بوخی توسعه یافته) برای این تبدیل مطرح شد.

تعریف رسمی[ویرایش]

به طور رسمی یک ماشین بوخی توسعه یافته یک چند تایی $A=(\phi ,\Sigma ,\Delta ,\phi _{0},\left\{F_{1},...,F_{n}\right\})$ است که شامل اجزاء زیر است:

φ یک مجموعهٔ متناهی است. مولفه‌های φ را حالتهای A می‌نامند.
Σ یک مجموعهٔ متناهی است که آنرا الفبای A می‌نامند.
$\Delta :\phi *\Sigma \rightarrow 2^{\phi }$ یک تابع است که آنرا رابطه انتقال A می‌نامند.
$\phi _{0}$ یک زیرمجموعه از φ است که حالتهای اولیه نامیده می‌شود.
${F_{1},...,F_{n}}$ که برای هر $1\leq i\leq n$ داریم $F_{i}\subseteq \phi$ ، شرط پذیرش است.

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

ماشین بوخی توسعه یافته برچسب دار[ویرایش]

ماشین بوخی توسعه یافته برچسب دار(LGBA)یک گونهٔ دیگر است که در آن ورودی به عنوان برچسب‌هایی با حالات به جای برچسب‌های با انتقال‌ها، همراه است. ماشین بوخی توسعه یافته برچسب دارتوسط گرس و همکارانش معرفی شد. به طور رسمی، یک ماشین بوخی توسعه یافته برچسب دار یک چند تایی $A=(\phi ,\Sigma ,L,\Delta ,\phi _{0},\left\{F_{1},...,F_{n}\right\})$ است که شامل اجزاء زیر است:

φ یک مجموعهٔ متناهی است. مولفه‌های φ را حالتهای A می‌نامند.
Σ یک مجموعهٔ متناهی است که آنرا الفبای A می‌نامند.
$L:\phi \rightarrow 2^{\Sigma }$ یک تابع است که آنرا تابع برچسب A می‌نامند.
$\Delta :\phi *\Sigma \rightarrow 2^{\phi }$ یک تابع است که آنرا رابطه انتقال A می‌نامند.
$\phi _{0}$ یک زیرمجموعه از φ است که حالتهای اولیه نامیده می‌شود.
$\left\{F_{1},...,F_{n}\right\}$ که برای هر $1\leq i\leq n$ داریم $F_{i}\subseteq \phi$ ، شرط پذیرش است.

فرض کنید $w=a_{1}a_{2}...$ یک ω-حرف روی الفبایΣباشد. حال $r_{1},r_{2},...$ یک چرخهٔ اجرا از A روی حرفw است اگر $r_{1}\in \phi _{0}$ و برای هر $i\geq 0$ داشته باشیم $r_{i+1}\in \Delta \left(r_{i}\right)$ و $a_{i}\in L\left(r_{i}\right)$ .