Кіріспе
Компьютерлік жүйелерді формалды тексеруде қолданылатын техника. Компьютер ғылымында, жартылай реттілік азайту – модельді тексеру немесе автоматтандырылған жоспарлау және кестелеу алгоритмімен ізделетін күй кеңістігінің мөлшерін азайту тәсілі. Ол, бір мезгілде орындалатын, бірақ әртүрлі ретпен орындалған өтулердің коммутативті қасиетін пайдаланады, нәтижесінде бірдей күйге жетеді. Күй кеңістігін тікелей зерттеуде, жартылай реттілік азайту әдетте барлық мүмкіндік алған өтулердің өкілдік жиынтығын кеңейтудің нақты тәсілін білдіреді. Бұл тәсіл сондай-ақ өкілдер арқылы модельді тексеру деп те сипатталады. Әдістің әртүрлі нұсқалары бар, мысалы, қатаң жиынтық әдісі, кең жиынтық әдісі.
In computer science, partial order reduction is a technique for reducing the size of the state space to be searched by a model checking or automated planning and scheduling algorithm. It exploits the commutativity of concurrently executed transitions that result in the same state when executed in different orders. In explicit state space exploration, partial order reduction usually refers to the specific technique of expanding a representative subset of all enabled transitions. This technique has also been described as model checking with representatives. There are various versions of the method, the so called stubborn set method, ample set method,
Қиындықтар жиынтығы
Қиын жиынтықтар нақты тәуелсіздік қатынасын қолданбайды. Керісінше, олар тек амалдар тізбектеріндегі ауыстырымдық қасиет арқылы анықталады. Егер келесі шарттар орындалса, жиын s-те (әлсіз) қасарысқан болады. D0, егер тізбекті орындау мүмкін болса және ол күйіне жеткізсе, онда тізбекті орындау мүмкін және ол күйіне жеткізеді. D1, немесе күйі туық нүкте болып табылады, немесе күйіне жету үшін орындалуы мүмкін. Бұл шарттар барлық туық нүктелерді сақтау үшін жеткілікті, дәл сияқты C0 және C1 кең жиынтық әдісінде. Дегенмен, олар сәл әлсіз, сондықтан кіші жиынтықтарға әкелуі мүмкін. C2 және C3 шарттары кең жиынтық әдісімен салыстырғанда одан да әлсіретілуі мүмкін, бірақ қасарысқан жиынтық әдісі C2 және C3 шарттарымен үйлесімді.
D1 Either is a deadlock, or such that , the execution of is possible. These conditions are sufficient for preserving all deadlocks, just like C0 and C1 are in the ample set method. They are, however, somewhat weaker, and as such may lead to smaller sets. The conditions C2 and C3 can also be further weakened from what they are in the ample set method, but the stubborn set method is compatible with C2 and C3.
Басқалар
Сондай-ақ, ішінара реттік азайтуды белгілеудің басқа да тәсілдері бар. Көбінесе қолданылатын әдістердің бірі – тұрақты жиын / ұйықтау жиыны алгоритмі. Толық ақпарат Патрис Годфройдтың диссертациясында келтірілген. Символдық модельді тексеруде, ішінара реттік азайту қосымша шектеулер (қорғау күшейту) қосу арқылы жүзеге асырылуы мүмкін. Ішінара реттік азайтудың тағы бір қолданылу саласы – автоматтандырылған жоспарлау.