b'\n_START_ARTICLE_\nModeli\xc5\xb3 tikrinimas\n_START_SECTION_\nAp\xc5\xbevalga\n_START_PARAGRAPH_\nSvarb\xc5\xabs modelio patikrinimo metodai buvo sukurti, kad j\xc5\xb3 pagalba b\xc5\xabt\xc5\xb3 galima patikrinti technin\xc4\x97s \xc4\xafrangos ir programin\xc4\x97s \xc4\xafrangos modelius, kuriuose reikalavimai yra i\xc5\xa1reik\xc5\xa1ti laikinos login\xc4\x97s formul\xc4\x97s pagalba. Novatori\xc5\xa1kas laikinos login\xc4\x97s formul\xc4\x97s modelio patikrinimo darbas buvo sukurtas E. M. Clarke ir E. A. Emerson bei J. P. Queille ir J. Sifakis. Clarke, Emerson ir Sifakis gavo bendr\xc4\x85 Turing apdovanojim\xc4\x85 u\xc5\xbe j\xc5\xb3 darb\xc4\x85 modelio patikrinimo srityje. Modelio patikrinimas yra da\xc5\xbeniausiai naudojamas patikrinant technin\xc4\x97s \xc4\xafrangos model\xc4\xaf. Dirbant su programine \xc4\xafranga d\xc4\x97l netikrumo (\xc5\xbei\xc5\xabr\xc4\x97kite apskai\xc4\x8diavimo teorij\xc4\x85) metodas negali b\xc5\xabti pilnai algoritminis; paprastai jis gali nepatvirtinti arba klaidingai patvirtinti reikiam\xc4\x85 savyb\xc4\x99. Strukt\xc5\xabra paprastai yra suvokiama kaip pirminis kodinis apib\xc5\xabdinimas, i\xc5\xa1reik\xc5\xa1tas pramonine technin\xc4\x97s \xc4\xafrangos apra\xc5\xa1om\xc4\x85ja kalba arba specialios paskirties kalba. Tokia programa atitinka ribotos b\xc5\xabsenos ma\xc5\xa1in\xc4\x85 (FSM), pvz., adresuotoje grafoje yra mazgai (arba vir\xc5\xa1\xc5\xabn\xc4\x97s) ir briaunos. Atomini\xc5\xb3 teigini\xc5\xb3 grup\xc4\x97 yra susijusi su kiekvienu mazgu, paprastai rodo, kurie atminties elementai yra \xc4\xafjungti. Mazgai rei\xc5\xa1kia sistemos b\xc5\xabsenas, briaunos rei\xc5\xa1kia galimus per\xc4\x97jimus, kurie gali keisti b\xc5\xabsen\xc4\x85, tuo tarpu atominiai teiginiai i\xc5\xa1rei\xc5\xa1kia esmines savybes, kurios u\xc5\xbetikrina darbo eig\xc4\x85. Paprastai, problema gali b\xc5\xabti i\xc5\xa1rei\xc5\xa1kiama taip: turime norim\xc4\x85 savyb\xc4\x99, i\xc5\xa1reik\xc5\xa1t\xc4\x85 kaip laikin\xc4\x85 logi\xc5\xa1k\xc4\x85 formul\xc4\x99 p, ir strukt\xc5\xabra M su pirmine b\xc5\xabsena s, apskai\xc4\x8diuokite, ar M, sI= p. Jei M yra galutin\xc4\x97, kaip yra technin\xc4\x97je \xc4\xafrangoje, modelio patikrinimas susiaur\xc4\x97ja iki grafos paie\xc5\xa1kos.'