Logik Dinamik Cadangan

Isi kandungan:

Logik Dinamik Cadangan
Logik Dinamik Cadangan

Video: Logik Dinamik Cadangan

Video: Logik Dinamik Cadangan
Video: Логический анализатор с Алиэкспресс, клон Saleae Logic 2024, Mac
Anonim

Navigasi Masuk

  • Kandungan Penyertaan
  • Bibliografi
  • Alat Akademik
  • Pratonton PDF Rakan
  • Maklumat Pengarang dan Petikan
  • Kembali ke atas

Logik Dinamik Cadangan

Pertama kali diterbitkan pada 1 Februari 2007; semakan substantif Jum 25 Jan 2019

Logik program adalah logik modal yang timbul dari idea untuk mengaitkan dengan setiap program komputer α bahasa pengaturcaraan suatu modaliti [α]. Idea ini berpunca dari karya karya Engeler [1967], Hoare [1969], Yanov [1959], dan lain-lain yang merumuskan dan mempelajari bahasa logik di mana sifat penyambung program dapat dinyatakan. Logik algoritma (AL) pertama kali dikembangkan oleh Salwicki [1970] dan logik dinamik (DL) yang dihuraikan oleh Pratt [1976] adalah kesinambungan karya-karya ini. Kami di sini akan menumpukan perhatian pada DL. Banyak makalah yang dikhaskan untuk DL dan variannya serta pelbagai aplikasi dalam pengesahan program dan struktur data menunjukkan bahawa ia merupakan alat yang berguna dalam mempelajari sifat program. Pratt memilih untuk menggambarkan DL mengenai apa yang boleh disebut tahap pertama,dan karyanya inilah yang memicu Fischer dan Ladner [1979] untuk menentukan varian proposisi DL beberapa tahun kemudian. Artikel ini memaparkan pengenalan kepada PDL, varian proposional DL.

  • 1. Pengenalan
  • 2. Definisi dan keputusan asas

    • 2.1 Sintaks dan semantik
    • 2.2 Aksiomatisasi dan kelengkapan
    • 2.3 Kerentanan dan kerumitan
  • 3. Pengaturcaraan berstruktur dan kebenaran program

    • 3.1 Kalkulus Hoare
    • 3.2 Hoare calculus dan PDL
    • 3.3 Jumlah betul
  • 4. Beberapa varian

    • 4.1 PDL tanpa ujian
    • 4.2 PDL dengan sebaliknya
    • 4.3 PDL dengan berulang dan gelung
    • 4.4 PDL dengan persimpangan
  • 5. Kesimpulan
  • Bibliografi
  • Alat Akademik
  • Sumber Internet Lain
  • Penyertaan Berkaitan

1. Pengenalan

Dynamic Logics (DL) adalah logik modal untuk mewakili keadaan dan peristiwa sistem dinamik. Bahasa DL adalah bahasa penegasan yang dapat menyatakan sifat keadaan pengiraan, dan bahasa pengaturcaraan yang dapat menyatakan sifat peralihan sistem antara keadaan ini. DL adalah logik program, dan izin untuk bercakap dan memberi alasan mengenai keadaan, proses, perubahan, dan hasil.

Logik dinamik program Pratt yang asli adalah logik mod pesanan pertama. Propositional Dynamic Logic (PDL) adalah rakan sepadannya. Itu dikemukakan sebagai logik dengan sendirinya dalam Fischer dan Ladner [1979]. Sebagai proporsional, bahasa PDL tidak menggunakan istilah, predikat, atau fungsi. Oleh itu, dalam PDL, terdapat dua kategori sintaksis: cadangan dan program.

Untuk memberi makna kepada pernyataan dalam PDL, kami biasanya bekerja dengan semantik abstrak dari segi Labeled Transition Systems (LTS). LTS dapat dilihat sebagai generalisasi model Kripke, di mana peralihan antara dunia, atau negara, "dilabel" dengan nama program atom. Penilaian menunjukkan untuk setiap negeri apa cadangan yang benar di dalamnya. Peralihan berlabel π dari satu keadaan x ke keadaan y-dicatatkan x R (π) y, atau (x, y) ∈ R (π)-menunjukkan bahawa bermula di x, ada kemungkinan pelaksanaan program π yang selesai di y. Sekiranya proposisi A benar dalam y, maka formula A adalah benar dalam x: iaitu, dalam keadaan x ada kemungkinan pelaksanaan program α yang berakhir pada keadaan yang memuaskan A. Seseorang mengenali dalam modaliti yang mengingatkan pada modaliti kemungkinan (sering diperhatikan ◊) logik modal. Tidak menghairankan,ada juga pengertian mengenai keperluan (yang modalnya sering diperhatikan □). Rumus [π] A akan berlaku dalam keadaan x jika A benar di setiap keadaan yang dapat dicapai dari x dengan peralihan berlabel π.

Kemungkinan pelaksanaan program yang kompleks dapat ditentukan seterusnya secara komposisi. Sebagai contoh, program "pertama α, kemudian β" adalah program yang kompleks, lebih khusus urutan. Pelaksanaan yang mungkin dapat ditunjukkan dalam LTS dengan menyusun peralihan dua langkah - oleh itu peralihan yang dapat ditandakan oleh R (α; β) - antara keadaan x dan x ': ada kemungkinan pelaksanaan dalam x program α yang selesai dalam keadaan y dan ada kemungkinan pelaksanaan dalam y program β yang selesai dalam x '. Sekiranya dalil A benar dalam x ', maka formula A akan benar dalam keadaan x. Program α dan β boleh menjadi program yang kompleks sendiri. Namun lebih banyak program dapat dinyatakan dengan lebih banyak konstruk yang akan kami sampaikan pada waktunya.

Program kemudian dilihat secara ekstensif: ia adalah hubungan binari antara pasangan keadaan LTS. Tepatnya, ini adalah set pasangan bentuk (x, y) sehingga program dapat dijalankan dalam keadaan x dan dapat menyebabkan keadaan y. Sebaliknya, dalil adalah pernyataan mengenai keadaan; sama ada benar atau salah dalam keadaan. Oleh itu, suatu cadangan juga dapat dilihat secara ekstensif: kumpulan keadaan LTS di mana ia benar.

Dengan akronim PDL, di sini kita merujuk tepat pada logik dinamik proposisi dengan konstruk program berikut: urutan, pilihan non-deterministik, iterasi tanpa batasan, dan ujian. Kami membentangkannya di bahagian 2, bersama dengan beberapa sifat dan hasil asas. Khususnya, kami akan menangani aksiomatisasi dan kebolehpecahannya.

Kalkulus Hoare dari Hoare [1969] adalah mercu tanda logik program. Ini menyangkut kebenaran penyataan bentuk {A} α {B} -berarti bahawa dengan prasyarat A program α selalu mempunyai B sebagai keadaan selepas keadaan-dan didefinisikan secara aksiomatik. Ini datang dari keinginan kaedah yang ketat untuk memikirkan sifat-sifat program, dan dengan itu memberi kepada aktiviti memprogram tempat tertentu dalam bidang sains. Burstall [1974] melihat analogi antara logika modal dan penaakulan tentang program, tetapi kerja sebenarnya di atasnya bermula dengan Pratt [1976] ketika ia dicadangkan kepadanya oleh R. Moore, seorang pelajarnya pada masa itu. PDL berasal dari tafsiran Pratt mengenai kalkulus Hoare dalam formalisme logik modal. Pengenalan genesis PDL boleh didapati di Pratt [1980b]. Hoare-triple {A} α {B} ditangkap oleh formula PDL A → [α] B yang secara harfiah bermaksud bahawa jika A benar, maka setiap kejayaan penghentian pelaksanaan α akan berakhir dengan B menjadi benar. Dengan hubungan ini dapat dicapai, adalah rutin untuk membuktikan peraturan awal kalkulus Hoare menggunakan eksklusif aksiomatisasi PDL. Ini adalah sesuatu yang akan kita lakukan secara terperinci di bahagian 3 yang memusatkan perhatian pada penaakulan mengenai kebenaran program tersusun.

Topik tambahan yang berkaitan dengan PDL termasuk hasil mengenai kekuatan ekspresi komparatif, kerentanan, kerumitan, dan kelengkapan sejumlah varian menarik yang diperoleh dengan memperluas atau membatasi PDL dengan berbagai cara. Sejak penubuhannya, banyak varian PDL telah mendapat perhatian. Varian ini mungkin mempertimbangkan program deterministik, ujian terhad, program tidak biasa, program sebagai automata, pelengkap dan persimpangan program, perhitungan berbalik dan tidak terbatas, dan lain-lain. Kami akan memaparkan beberapa di antaranya di bahagian 4, memberikan beberapa petunjuk mengenai ekspresi relatif mereka, aksiomatisasi mereka, dan kerumitan komputasi mereka.

Kami membuat kesimpulan dalam bahagian 5.

2. Definisi dan keputusan asas

Kami memaparkan sintaksis dan semantik PDL di bahagian 2.1. Teori bukti PDL disajikan dalam bahagian 2.2 dengan aksiomatisasi dan menunjukkan kepada literatur mengenai kelengkapan. Kami menangani masalah kerentanan dan kerumitan di bahagian 2.3.

2.1 Sintaks dan semantik

Logik dinamik cadangan (PDL) direka untuk mewakili dan menaakul tentang sifat cadangan program. Sintaksnya berdasarkan dua set simbol: satu set yang dapat dikira Φ 0 formula atom dan satu set yang dapat dikira Π 0 dari program atom. Rumusan rumit dan program rumit di dasar ini ditakrifkan sebagai berikut:

  • Setiap formula atom adalah formula
  • 0 ("false") adalah formula
  • Sekiranya A adalah formula maka ¬ A ("bukan A") adalah formula
  • Sekiranya A dan B adalah formula maka (A ∨ B) ("A atau B") adalah formula
  • Sekiranya α adalah program dan A adalah formula maka [α] A ("setiap pelaksanaan α dari keadaan sekarang membawa ke keadaan di mana A benar") adalah formula
  • Setiap program atom adalah program
  • Sekiranya α dan β adalah program maka (α; β) ("do α diikuti oleh β") adalah program
  • Sekiranya α dan β adalah program maka (α∪β) ("lakukan α atau β, tidak ditentukan") adalah program,
  • Sekiranya α adalah program maka α * ("ulangi α yang terhingga, tetapi ditentukan secara tidak ditentukan, berapa kali") adalah program.
  • Sekiranya A adalah formula maka A? ("Lanjutkan jika A benar, yang lain gagal") adalah program

Penghubung Boolean lain 1, ∧, →, dan ↔ digunakan sebagai singkatan dengan cara standard. Sebagai tambahan, kami menyingkat ¬ [α] ¬ A ke A ("beberapa pelaksanaan α dari keadaan sekarang mengarah ke keadaan di mana A benar") seperti dalam logika modal. Kami menulis α n untuk α;…; α dengan n kejadian α. Lebih formal:

  • α 0 = df 1?
  • α n +1 = df α; α n

Juga:

α + = df α; α *

sering berguna untuk mewakili lelaran yang tidak terikat tetapi berlaku sekurang-kurangnya sekali. Akhirnya, kami menggunakan peraturan standard untuk menghilangkan tanda kurung.

Rumus dapat digunakan untuk menggambarkan sifat-sifat yang ada setelah kejayaan pelaksanaan program. Sebagai contoh, formula [α∪β] A bermaksud bahawa setiap kali program α atau β berjaya dilaksanakan, keadaan dicapai di mana A menahan, sedangkan formula A bermaksud bahawa terdapat urutan pelaksanaan gantian α dan β sehingga keadaan dicapai di mana A memegang. Secara semantik, formula ditafsirkan oleh set keadaan dan program ditafsirkan oleh hubungan binari ke atas negeri dalam sistem peralihan. Lebih tepat lagi, makna formula dan program PDL ditafsirkan melalui Labeled Transition Systems (LTS) M = (W, R, V) di mana W adalah sekumpulan dunia atau keadaan yang tidak dilupakan, R adalah pemetaan dari set Π 0 atom program ke dalam hubungan binari pada W dan V adalah pemetaan dari set Φ 0 formula atom menjadi subkumpulan W.

Secara tidak formal, pemetaan R memberikan kepada setiap program atom π ∈ Π 0 beberapa hubungan binari R (π) pada W dengan makna yang dimaksudkan x R (π) y jika terdapat pelaksanaan π dari x yang mengarah ke y, sedangkan pemetaan V memberikan kepada setiap formula atom p ∈ Φ 0 beberapa subset V (p) W dengan makna yang dimaksudkan x ∈ V (p) iff p adalah benar dalam x. Memandangkan pembacaan kami dari 0, ¬ A, A ∨ B, [α] A, α; β, α∪β, α * dan A?, Jelas bahawa R dan V mesti diperluas secara induktif sebagai berikut untuk memberikan maksud yang dimaksudkan untuk program dan formula yang kompleks:

  • x R (α; β) y sekiranya terdapat dunia z sehingga x R (α) z dan z R (β) y
  • x R (α∪β) y iff x R (α) y atau x R (β) y
  • x R (α *) y sekiranya terdapat bilangan bulat bukan negatif n dan wujud dunia z 0,…, z n sehingga z 0  = x, z n  = y dan untuk semua k = 1.. n, z k −1 R (α) z k
  • x R (A?) y iff x = y dan y ∈ V (A)
  • V (0) = ∅
  • V (¬ A) = W / V (A)
  • V (A ∨ B) = V (A) ∪ V (B),
  • V ([α] A) = {x: untuk semua dunia y, jika x R (α) y maka y ∈ V (A)}

Sekiranya x ∈ V (A) maka kita mengatakan bahawa A berpuas hati pada keadaan x dalam M, atau "M, x sat A".

Dua LTS dua hala
Dua LTS dua hala

Panggil M LTS yang digambarkan di atas di sebelah kiri dan M 'LTS yang digambarkan di sebelah kanan. Secara formal, kami mempunyai M = (W, R, V) dengan W = {x 1, x 2 }, R (π 1) = {(x 1, x 1)}, R (π 2) = {(x 1, x 2)}, V (p) = {x 1 }, V (q) = {x 2 }, dan kami mempunyai M '= (W', R ', V') dengan W '= {y 1, y 2, y 3, y 4 }, R (π 1) = {(y 1, y 2), (y 2, y 2)}, R '(π2) = {(y 1, y 3), (y 2, y 4)}, V '(p) = {y 1, y 2 }, V' (q) = {y 3, y 4 }. Kami mempunyai contoh:

  • M, x 1 sat p
  • M, x 2 sat q
  • M, x 1 sat <π 1 > p ∧ <π 2 > q
  • M, x 1 sat [π 1] p ∧ [π 1 *] p
  • M ', y 1 sat <π 1 *; π 2 > q
  • M ', y 2 sat [π 1 *] p
  • M ', y 1 sat [π 1 ∪π 2] (q ∨ p)
  • M ', y 3 sat [π 1 ∪π 2] 0

Sekarang pertimbangkan formula A. Kami mengatakan bahawa A berlaku di M atau bahawa M adalah model A, atau "M ⊨ A", jika semua dunia x, x ∈ V (A). A dikatakan sah, atau "⊨ A", jika berlaku untuk semua model M, M ⊨ A. Kami mengatakan bahawa A memenuhi syarat di M atau M memenuhi A, atau "M sat A", jika ada dunia x sehingga x ∈ V (A). A dikatakan puas, atau "sat A", jika ada model M sedemikian rupa sehingga M duduk A. Menariknya,

sat A iff not ¬ A A A

iff not sat ¬ A

Beberapa formula PDL yang luar biasa berlaku. (Pembaca boleh mencuba membuktikannya secara formal, atau sekurang-kurangnya mula meyakinkan diri mereka pada beberapa contoh yang ditunjukkan di atas.)

⊨ [α; β] A ↔ [α] [β] A

⊨ [α∪β] A ↔ [α] A ∧ [β] A

⊨ [α *] A ↔ A ∧ [α] [α *] A

⊨ [A?] B ↔ (A → B)

Sama, kita boleh menuliskannya dalam bentuk ganda mereka.

⊨ A ↔ A

⊨ A ↔ A ∨ A

⊨ A ↔ A ∨ A

⊨ <A?> B ↔ A ∧ B

Satu pengertian menarik mengenai jumlah maklumat, dinyatakan dengan formula PDL, yang terkandung dalam LTS. Tingkah laku sistem yang digambarkan sebagai LTS memang sering tersembunyi dalam bentuknya. Sebagai contoh, pada pemeriksaan sederhana, mudah untuk meyakinkan diri sendiri bahawa dua LTS yang digambarkan di atas mempunyai tingkah laku yang sama, dan memenuhi formula PDL yang sama. Untuk menyelesaikan bahagian ini mengenai sintaks dan semantik, kami memberikan asas teori tuntutan ini.

Memandangkan dua LTS, seseorang mungkin bertanya sama ada mereka memenuhi formula yang sama. Gagasan bisimulasi telah menjadi ukuran standar untuk kesetaraan model Kripke dan Sistem Peralihan Berlabel. Bisimulasi antara LTSs M = (W, R, V) dan M '= (W', R ', V') adalah hubungan binari Z antara keadaan mereka sehingga untuk semua dunia x di M dan untuk semua dunia x ' dalam M ', jika xZx' maka

  • untuk semua formula atom p ∈ Φ 0, x ∈ V (p) iff x '∈ V' (p)
  • untuk semua program atom π ∈ Π 0 dan untuk semua dunia y di M, jika x R (π) y maka ada dunia y 'di M' sehingga yZy 'dan x' R '(π) y'
  • untuk semua program atom π ∈ Π 0 dan untuk semua dunia y 'di M', jika x 'R' (π) y 'maka wujud dunia y di M sehingga yZy' dan x R (π) y

Kami mengatakan bahawa dua LTS adalah serupa apabila terdapat bimulasi di antara mereka. Telah diketahui sejak awal PDL bahawa dalam dua LTSs dua M dan M ', untuk semua dunia x di M dan untuk semua dunia x' di M ', jika xZx' maka untuk semua formula PDL A, x ∈ V (A) iff x '∈ V' (A). Oleh itu, apabila dua LTS sama seperti di bawah definisi bisimulasi di atas, maka, sekiranya xZx 'maka

  • untuk semua program α dan untuk semua dunia y di M, jika x R (α) y maka ada dunia y 'di M' sehingga yZy 'dan x' R '(α) y'
  • untuk semua program α dan untuk semua dunia y 'di M', jika x 'R' (α) y 'maka ada dunia y di M sehingga yZy' dan x R (α) y

Oleh itu seseorang hanya boleh membandingkan tingkah laku dua LTS dengan memeriksa program atom semata-mata dan dengan selamat membuat pernyataan mengenai tingkah laku perbandingan LTS ini walaupun untuk program yang kompleks. Kami mengatakan bahawa konstruksi program PDL selamat untuk bisimulasi. Lihat Van Benthem [1998] untuk pencirian tepat aturcara program yang selamat untuk bisimulasi.

Dengan mudah dilihat bahawa dua kejadian LTS di atas adalah serupa. Bisimulasi Z antara M dan M 'boleh diberikan sebagai: Z = {(x 1, y 1), (x 1, y 2), (x 2, y 3), (x 2, y 4)}. Negeri x 1 dan y 1 memenuhi formula PDL yang sama. Begitu juga keadaan x 1 dan y 2, dll.

2.2 Aksiomatisasi dan kelengkapan

Tujuan teori pembuktian adalah untuk memberikan pencirian harta benda ⊨ A dari segi aksioma dan peraturan inferens. Dalam bahagian ini, kami mendefinisikan predikat deducibility ⊢ secara induktif oleh operasi pada formula yang hanya bergantung pada struktur sintaksisnya sedemikian rupa sehingga untuk semua formula A,

I A iff ⊨ A.

Sudah tentu, PDL adalah lanjutan dari logik proposisi klasik. Kami pertama kali mengharapkan bahawa semua tautologi proposisi berlaku, dan semua penaakulan proposional dibenarkan. Khususnya, modus ponens adalah peraturan yang sah: dari A dan A → B menyimpulkan B. Untuk mana-mana program α, membatasi LTS ke hubungan R (α) kita memperoleh model Kripke di mana logik modaliti [α] adalah logik mod normal cadangan yang paling lemah, iaitu logik K. Oleh itu, PDL mengandungi setiap kejadian skema aksioma pengedaran yang biasa:

(A0) [α] (A → B) → ([α] A → [α] B)

dan ditutup dengan peraturan inferensi berikut (peraturan keperluan):

(N) dari A infer [A] A.

Logik modal adalah normal jika mematuhi (A0) dan (N). Sifat-sifat penting untuk semua α, adalah bahawa [α] menyebar melalui konjungsi ∧, dan peraturan monoton, yang membenarkan dari A → B untuk membuat kesimpulan [α] A → [α] B, dapat dibuktikan. Akhirnya, PDL adalah logik modal yang paling tidak normal yang mengandungi setiap contoh skema aksioma berikut

(A1) [α; β] A ↔ [α] [β] A

(A2) [α∪β] A ↔ [α] A ∧ [β] A

(A3) [α *] A ↔ A ∧ [α] [α *] A

(A4) [A?] B ↔ (A → B)

dan ditutup di bawah peraturan inferensi berikut (peraturan invariance gelung):

(I) dari A → [α] A menyimpulkan A → [α *] A

Sekiranya X adalah sekumpulan formula dan A adalah formula, maka kita mengatakan bahawa A dapat dikurangkan from dari X, atau "X ⊢ A", jika terdapat urutan A 0, A 1,…, A n formula sedemikian sehingga A n  = A dan untuk semua i ≤ n, A i adalah contoh skema aksioma, atau formula X, atau berasal dari formula urutan sebelumnya dengan aturan inferensi. Selanjutnya, ⊢ A iff ∅ ⊢ A; dalam kes ini kita mengatakan bahawa A tidak boleh dikurangkan ⊢. X dikatakan konsisten ff jika tidak X ⊢ 0. Sangat mudah untuk menetapkan bahawa (I) dapat digantikan oleh skema aksioma berikut (skema aksioma induksi):

(A5) [α *] (A → [α] A) → (A → [α *] A)

Mari kita tentukan terlebih dahulu bahawa (I) adalah peraturan turunan sistem bukti berdasarkan (A1), (A2), (A3), (A4) dan (A5):

1. A → [α] A premis
2. [α *] (A → [α] A) dari 1 menggunakan (N)
3. [α *] (A → [α] A) → (A → [α *] A) skema aksioma (A5)
4. A → [α *] A dari 2 dan 3 menggunakan modus ponens

Mari kita seterusnya menetapkan bahawa (A5) tidak dapat dikurangkan:

1. [α *] (A → [α] A) ↔ (A → [α] A) ∧ [α] [α *] (A → [α] A) skema aksioma (A3)
2. A ∧ [α *] (A → [α] A) → [α] (A ∧ [α *] (A → [α] A)) dari 1 menggunakan penaakulan proporsional dan penyebaran [α] lebih ∧
3. A ∧ [α *] (A → [α] A) → [α *] (A ∧ [α *] (A → [α] A)) dari 2 menggunakan (I)
4. [α *] (A → [α] A) → (A → [α *] A) dari 3 menggunakan penaakulan proporsional dan penyebaran [α *] lebih ∧

Aksiomatisasi PDL berdasarkan skema aksioma (A1), (A2), (A3), (A4) dan (A5) telah dicadangkan di Segerberg [1977]. Dari definisi di atas, ⊢ adalah baik berkenaan dengan ⊨, iaitu

Untuk semua formula A, jika ⊢ A, maka ⊨ A

Pembuktian diteruskan dengan induksi pada panjang pemotongan A dalam ⊢. Persoalan mengenai kelengkapan ⊢ sehubungan dengan ⊨, iaitu,

Untuk semua formula A, jika ⊨ A, maka ⊢ A

dikejar oleh beberapa ahli logik. Garis penaakulan yang dikemukakan dalam Segerberg [1977] adalah percubaan pertama untuk membuktikan kelengkapan ⊢. Tidak lama kemudian, Parikh juga membawa bukti. Ketika awal 1978 Segerberg menemui kekurangan dalam argumennya (yang akhirnya diperbaiki), Parikh menerbitkan apa yang boleh dianggap sebagai bukti pertama tentang kelengkapan ⊢ dalam Parikh [1978]. Bukti kelengkapan Different yang berbeza telah diterbitkan sejak, misalnya Kozen dan Parikh [1981].

Teori bukti alternatif yang berbeza dari PDL juga telah dicari. Bahkan pada awalnya, terutamanya di Pratt [1978]. Mari kita kemudian menyebutkan kelengkapan teori yang berkaitan oleh Nishimura [1979] dan Vakarelov [1983].

Rumusan alternatif predikat deduktif untuk PDL membenarkan penggunaan aturan inferensi infiniter, seperti dalam Goldblatt [1992a]. (Aturan inferensi infiniter memerlukan bilangan premis yang tidak terhingga.) Mari pred 'menjadi predikat deducibility yang sesuai dalam bahasa logik dinamik proporsional ke logik modal paling tidak normal yang mengandungi setiap contoh skema aksioma (A1), (A2), (A3) dan (A4) dan ditutup di bawah peraturan inferensi infiniter berikut:

(I ') dari {[β] [α n] A: n ≥ 0} simpulkan [β] [α *] A

Ini dapat dibuktikan bahawa ⊢ 'baik dan lengkap dengan hormat ⊨, iaitu,

Untuk semua formula A, A 'A iff ⊨ A

Dengan kata lain, sejauh menghasilkan set semua formula yang sahih, sistem bukti ⊢ dan ⊢ 'adalah setara.

2.3 Kerentanan dan kerumitan

Tujuan teori kerumitan adalah untuk menentukan pengiraan harta tanah A dari segi sumber masa atau ruang. Kerumitan logik L sering diidentifikasi dengan masalah menentukan kesesuaian formula, yang ditakrifkan sebagai:

(L-SAT) Diberi formula A dari L, apakah A dapat memuaskan?

Di bahagian ini, kami menyiasat kerumitan masalah keputusan berikut:

(PDL-SAT) Diberi formula A PDL, apakah A dapat memuaskan?

Aksiomatisasi lengkap PDL adalah definisi rekursif bagi sekumpulan formula PDL yang sah, atau dengan kata lain, dari sekumpulan formula yang penolakannya tidak memuaskan. Oleh itu, mengenai masalah (PDL-SAT), kami memiliki sub-prosedur yang akan menjawab "tidak" jika formula A PDL tidak memuaskan. Sub-prosedur (SP1) terdiri dalam menghitung semua formula ⊢-deducible, bermula dari aksioma dan menyimpulkan teorema lain dengan bantuan peraturan inferensi. Memandangkan masa yang cukup, jika formula tidak dapat dikurangkan, sub-prosedur akhirnya akan berjaya. Oleh itu, jika A tidak dapat dipenuhi, (SP1) akhirnya mesti mencari ¬ A, dan menjawab "tidak" bila ada.

Namun, jika formula A memuaskan, maka (SP1) tidak akan pernah menemui ¬ A. Ia akan berjalan selama-lamanya, dan seseorang tidak dapat memastikannya pada bila-bila masa. Tetapi ada jalan keluar dari ketidakpastian ini. Kita juga dapat memikirkan sub-prosedur kedua yang menjawab "ya" jika formula PDL memenuhi syarat. Sesungguhnya, salah satu hasil awal pada PDL adalah bukti bahawa PDL mempunyai harta model terhingga, iaitu,

Untuk semua formula A, jika duduk A maka ada model M terhingga sehingga M duduk A.

Properti model terhingga menawarkan asas untuk sub-prosedur (SP2) yang terdiri dalam menghitung satu persatu model PDL terhingga dan menguji sama ada salah satu daripadanya memenuhi formula. (Untuk semua formula A dan untuk semua model terhingga M, sangat mudah untuk menguji apakah M sat A dengan menerapkan definisi V (A).) Oleh itu, jika A memuaskan, akhirnya ia mesti mencari model M sehingga M sat A, dan jawab "ya" apabila ada. Secara simetris ke sub-prosedur pertama (SP1), jika formula A tidak memuaskan, maka (SP2) tidak akan pernah menemui model yang memuaskannya, ia akan berjalan selamanya, dan seseorang tidak dapat memastikannya pada bila-bila masa.

Sekarang, menggabungkan (SP1) dan (SP2) bersama-sama kita mempunyai cara untuk menentukan sama ada formula PDL A dapat memuaskan. Cukup untuk menjalankannya secara selari: jika A memenuhi syarat maka (SP2) akhirnya akan menjawab "ya", jika A tidak memenuhi syarat maka (SP1) akhirnya akan menjawab "tidak". Prosedur berhenti apabila (SP1) atau (SP2) memberikan jawapan.

Sekiranya prosedur yang diperoleh cukup untuk menyimpulkan bahawa masalahnya (PDL-SAT) dapat dipastikan, maka praktiknya sangat tidak berkesan. Terdapat hasil-akibat Fischer dan Ladner [1979] dan Kozen dan Parikh [1981] - lebih kuat daripada harta model terhingga, iaitu harta model kecil:

Untuk semua formula A, jika duduk A maka ada model M yang terhingga ukuran eksponensial dalam A sehingga M duduk A.

Ini bermaksud bahawa kita sekarang akan tahu kapan harus berhenti mencari model yang memuaskan formula dalam prosedur (SP2). Oleh itu, kita dapat menggunakan (SP2) untuk menguji apakah rumus dapat dipenuhi, tetapi setelah kita menghabiskan semua model kecil, kita dapat menyimpulkan bahawa rumus itu tidak memuaskan. Ini menghasilkan prosedur yang berjalan secara non-deterministik dalam waktu eksponensial (NEXPTIME): kira model ukuran paling eksponensial, dan periksa sama ada ia memenuhi formula. Tetapi hasil utama dalam teori kerumitan PDL berasal dari Fischer dan Ladner [1979] dan Pratt [1980a]. Dengan memerhatikan bahawa formula PDL dapat menerangkan dengan berkesan pengiraan mesin Turing bergantian dengan ruang-linier, Fischer dan Ladner [1979] pertama kali menetapkan batas bawah masa eksponen (PDL-SAT). Batas atas EXPTIME (PDL-SAT) telah diperoleh oleh Pratt [1980a],yang menggunakan setara untuk PDL kaedah tableaux. Oleh itu, (PDL-SAT) adalah LUAR BIASA-lengkap. (Algoritma yang lebih cekap dalam praktik, walaupun masih berjalan dalam waktu eksponen deterministik dalam keadaan terburuk, dicadangkan dalam De Giacomo dan Massacci [2000].)

3. Pengaturcaraan berstruktur dan kebenaran program

Dari segi sejarah, logik program berasal dari karya pada akhir tahun 1960-an para saintis komputer yang berminat untuk memberikan makna kepada bahasa pengaturcaraan dan mencari standard yang ketat untuk bukti mengenai program tersebut. Sebagai contoh, bukti seperti itu mengenai kebenaran program berkenaan dengan tingkah laku yang diharapkan, atau mengenai penghentian program. Kertas seminal adalah Floyd [1967] yang menyajikan analisis sifat program komputer berstruktur menggunakan carta alir. Beberapa karya awal seperti Yanov [1959] atau Engeler [1967] telah maju dan mempelajari bahasa formal di mana sifat penyambung program dapat dinyatakan. Formalisme Hoare [1969] merupakan tonggak dalam kedatangan PDL. Ini diusulkan sebagai tafsiran aksiomatik yang ketat terhadap carta alir Floyd. Kita sering bercakap mengenai logik Hoare, atau logik Floyd-Hoare,atau Hoare calculus ketika merujuk kepada formalisme ini. Hoare calculus berkaitan dengan kebenaran pernyataan ("Hoare triples"), seperti {A} α {B} yang mewujudkan hubungan antara prasyarat A, program α, dan pasca-syarat B. Ini menunjukkan bahawa setiap kali A memegang sebagai prasyarat pelaksanaan α, maka B berlaku sebagai syarat selepas kejayaan pelaksanaan α.

Ia berlaku beberapa dekad yang lalu, dan masih berlaku: mengesahkan program lebih kerap daripada tidak dilakukan dengan mengujinya pada pelbagai input yang masuk akal. Apabila input tidak menghasilkan output yang diharapkan, "bug" diperbaiki. Sekiranya akhirnya untuk setiap input yang diuji kita memperoleh output yang diharapkan, seseorang memiliki kepercayaan yang masuk akal bahawa program ini tidak memiliki kesalahan. Walau bagaimanapun, ini adalah kaedah pengesahan yang memakan masa, dan meninggalkan input yang belum diuji yang akan gagal. Mencari kesilapan ini setelah program dilaksanakan dan digunakan bahkan lebih mahal dari segi sumber. Beralasan mengenai kebenaran program dengan kaedah formal sangat penting untuk sistem kritikal kerana ia menawarkan cara membuktikan secara menyeluruh bahawa program tidak mempunyai kesalahan.

3.1 Kalkulus Hoare

Untuk menggambarkan jenis prinsip program yang ditangkap oleh peraturan dalam kalkulus Hoare, sudah cukup untuk meneliti beberapa di antaranya. (NB: peraturan bermaksud bahawa jika semua pernyataan di atas garis peraturan menahan-premis-maka juga pernyataan di bawah garis peraturan-kesimpulan-berlaku.)

{A} α 1 {B} {B} α 2 {C} (peraturan komposisi)
{A} α 1; α 2 {C}

Peraturan komposisi menangkap komposisi asas program yang berurutan. Sebagai premis, kami mempunyai dua andaian mengenai kebenaran separa dari dua program α 1 dan α 2. Andaian pertama adalah bahawa apabila α 1 dijalankan dalam keadaan memuaskan A, maka ia akan berakhir dalam keadaan memuaskan B, setiap kali berhenti. Andaian kedua adalah bahawa apabila α 2 dijalankan dalam keadaan memuaskan B, maka akan berakhir dalam keadaan memuaskan C, setiap kali berhenti. Kesimpulan peraturan adalah mengenai kebenaran separa program α 1; α 2 (iaitu, α 1 secara berurutan disusun dengan α 2), berikut dari dua andaian. Yaitu, kita dapat menyimpulkan bahawa jika α 1; α 2 dijalankan dalam keadaan yang memuaskan A, maka ia akan selesai dalam keadaan yang memuaskan C, setiap kali berhenti.

Peraturan iterasi adalah penting kerana menangkap kemampuan penting program untuk melaksanakan beberapa bahagian kod berulang kali sehingga keadaan tertentu tidak lagi berlaku.

{A ∧ B} α {A} (peraturan lelaran)
{A} sementara B melakukan α {¬ B ∧ A}

Akhirnya, kedua-dua peraturan konsekuensi adalah asas untuk memberi asas formal kepada penaakulan yang jelas secara intuitif yang melibatkan keadaan pasca lemah dan prasyarat yang lebih kuat.

{A} α {B} B → C (peraturan akibat 1)
{A} α {C}
C → A {A} α {B} (peraturan akibat 2)
{C} α {B}

Dari formalisme yang disajikan di Hoare [1969], kami meninggalkan skema aksioma kerana ia memerlukan bahasa orde pertama. Akhirnya, dalam karya seterusnya mengenai logik Hoare, lebih banyak peraturan juga sering ditambahkan. Lihat Apt [1979] untuk gambaran awal.

3.2 Hoare calculus dan PDL

Logik dinamik berasal dari tafsiran Pratt mengenai Hoare triples dan Hoare calculus dalam formalisme logik modal. Dengan modaliti [α], kita dapat menyatakan secara formal bahawa semua keadaan yang dapat dicapai dengan melaksanakan α memenuhi formula A. Ini dilakukan dengan menulis [α] A. Oleh itu, Hoare triple {A} α {B} hanya ditangkap oleh formula PDL

A → [α] B

Di samping itu, konstruk pengaturcaraan penting diperkenalkan dengan mudah dalam PDL dengan singkatan definisi:

  • jika A maka α lain β = df ((A?; α) ∪ (¬ A?; β))
  • sementara A do α = df ((A?; α) *; ¬ A?)
  • ulangi α hingga A = df (α; ((¬ A; α) *; A?))
  • batalkan = df 0?
  • langkau = df 1?

Oleh itu, nampaknya dengan PDL kita dilengkapi dengan baik untuk membuktikan secara logik kebenaran program berstruktur. Di luar hubungan yang agak melambaikan tangan antara PDL dan kalkulus Hoare, mungkin belum jelas bagaimana kaitannya secara formal. PDL sebenarnya merupakan generalisasi kalkulus Hoare dalam arti bahawa semua peraturan kalkulus Hoare dapat dibuktikan dalam sistem aksiomatik PDL. (Dengan bersungguh-sungguh, kalkulus Hoare mengandungi aksioma yang memerlukan bahasa lanjutan dari Logik Dinamik orde pertama.) Ini cukup luar biasa, jadi kami akan menunjukkan di sini dua peraturan di atas untuk dijadikan contoh.

Buktinya dimulakan dengan menganggap asas peraturan. Kemudian dengan menggunakan andaian, aksioma dan peraturan PDL ini, dan tidak lain, objektifnya adalah untuk menentukan bahawa kesimpulan peraturan mengikuti secara logik. Oleh itu, untuk aturan komposisi, kita mulakan dengan menganggap {A} α 1 {B}, iaitu A → [α 1] B dalam formulasi PDLnya, dan dengan menganggap {B} α 2 {C}, itu adalah B → [α 2] C. Objektifnya adalah untuk membuktikan bahawa {A} α 1; α 2 {C}. Tepatnya, kami ingin membuktikan bahawa A → [α 1; α 2] C dapat dikurangkan from dari kumpulan formula {A → [α 1] B, B → [α 2] C}.

1. A → [α 1] B andaian {A} α 1 {B}
2. B → [α 2] C andaian {B} α 2 {C}
3. 1] B → [α 1] [α 2] C Dari 2 menggunakan monoton [α 1]
4. A → [α 1] [α 2] C dari 1 dan 3 menggunakan penaakulan proposional
5. 1; α 2] C ↔ [α 1] [α 2] C skema aksioma (A1)
6. A → [α 1; α 2] C dari 4 dan 5 menggunakan penaakulan proposional
- {A} α 1; α 2 {C}

Bukti peraturan lelaran sedikit lebih terlibat.

1. A ∧ B → [α] A andaian {A ∧ B} α {A}
2. A → (B → [α] A) dari 1 menggunakan penaakulan proposional
3. [B?] [Α] A ↔ (B → [α] A) skema aksioma (A4)
4. A → [B?] [Α] A dari 2 dan 3 menggunakan penaakulan proposional
5. [B?; α] A ↔ [B?] [α] A skema aksioma (A1)
6. A → [B?; Α] A dari 4 dan 5 menggunakan penaakulan proposional
7. A → [(B?; Α) *] A dari 6 menggunakan (I)
8. A → (¬ B → (¬ B ∧ A)) tautologi cadangan
9. A → [(B?; Α) *] (¬ B → (¬ B ∧ A)) dari 7 dan 8 menggunakan monoton [(B?; α) *] dan penaakulan proposional
10. [¬ B?] (¬ B ∧ A) ↔ (¬ B → (¬ B ∧ A)) Skema aksioma (A4)
11. A → [(B?; Α) *] [¬ B?] (¬ B ∧ A) dari 9 dan 10 menggunakan monoton [(B?; α) *] dan penaakulan proposional
12. [(B?; Α) *; ¬ B?] (¬ B ∧ A) ↔ [(B?; Α) *] [¬ B?] (¬ B ∧ A) skema aksioma (A1)
13. A → [(B?; Α) *; ¬ B?] (¬ B ∧ A) dari 12 menggunakan penaakulan proposional
- {A} sementara B melakukan α {¬ B ∧ A}

Dalam konteks PDL, kedua-dua peraturan akibatnya adalah kes khas dari aturan komposisi. Untuk mendapatkan peraturan pertama, gantikan α 1 dengan α dan α 2 dengan langkau. Untuk mendapatkan peraturan kedua, gantikan α 1 dengan langkau dan α 2 dengan α. Cukup untuk menerapkan skema aksioma (A4), dan untuk menyatakan bahawa [α; langkau] A ↔ [α] A dan [α; skip] A ↔ [α] A juga ⊢-deducible untuk semua A dan semua α.

3.3 Jumlah betul

Dengan pengakuan Hoare di Hoare [1979], kalkulus asalnya hanyalah titik permulaan dan mengalami beberapa batasan. Terutama, hanya membenarkan seseorang membuat alasan mengenai kebenaran separa. Maksudnya, kebenaran pernyataan {A} α {B} hanya memastikan bahawa semua pelaksanaan a yang bermula dalam keadaan yang memuaskan A akan berakhir pada keadaan yang memuaskan B, atau tidak akan berhenti. Iaitu, program yang sebahagiannya betul mungkin mempunyai pelaksanaan yang tidak berakhir. (Sebenarnya, program yang tidak mempunyai pelaksanaan penutupan akan selalu betul sebahagiannya. Ini adalah contohnya untuk program semasa 1 melangkau. Rumus A → [ sementara 1 tidak lompat] B dapat dikurangkan untuk semua formula A dan B.) Kalkulus tidak memberikan asas untuk bukti bahawa program berakhir. Ia dapat diubah sehingga memperhitungkan kebenaran keseluruhan program: kebenaran separa dan penamatan. Ia dicapai dengan mengubah peraturan lelaran. Kami tidak membentangkannya di sini dan merujuk pembaca yang berminat ke Apt [1981].

Mari kita perhatikan terlebih dahulu bahawa untuk program deterministik, seseorang sudah dapat mengetahui kebenaran sepenuhnya melalui formula yang serupa

A → B

Ungkapan B bermaksud bahawa terdapat pelaksanaan α yang berakhir dalam keadaan yang memuaskan B. Lebih-lebih lagi, jika α adalah deterministik, kemungkinan pelaksanaan penamatan ini adalah pelaksanaan unik α. Oleh itu, jika seseorang berjaya membuktikan bahawa program itu bersifat deterministik, muslihat ini berfungsi dengan baik untuk membuktikan kebenarannya sepenuhnya.

Penyelesaian umum untuk masalah ketepatan total ada di dunia PDL. Tetapi kita perlu memanjangkannya sedikit. Pratt telah menyinggung dalam Pratt [1980b] bahawa PDL tidak cukup ekspresif untuk menangkap perulangan program yang tidak terbatas. Sebagai reaksi, PDL dengan mengulangi (RPDL) diperkenalkan oleh Streett [1982]. Ini berisi, untuk semua program α, ungkapan Δα bermaksud proposisi baru dengan semantik

V (Δα) = {x: terdapat urutan tak terhingga x 0, x 1,… keadaan sedemikian sehingga x 0  = x dan untuk semua n ≥ 0, x n R (α) x n +1 }

Streett [1982] menduga bahawa RPDL dapat di aksiomatikan dengan menambahkan sistem bukti PDL tepat skema aksioma berikut.

(A6) Δα → Δα

(A7) [α *] (A → A) → (A → Δα)

Bukti dugaan tersebut diberikan dalam Sakalauskaite dan Valiev [1990]. (Versi dugaan dalam varian gabungan PDL juga terbukti dalam Gargov dan Passy [1988].)

Sangat mudah untuk dilihat bahawa dalam kalkulus Hoare yang disajikan di atas, penamatan tidak hanya boleh datang dari peraturan lelaran. Secara analogi, penghentian program PDL hanya boleh berlaku daripada penggunaan lelaran tanpa had. Ungkapan Δα menunjukkan bahawa α * boleh menyimpang, dan ini hanya jenis tanggapan yang kita perlukan. Kita sekarang boleh menentukan predikat secara induktif ∞ sehingga untuk program α, formula ∞ (α) akan berlaku tepat ketika α dapat memasuki pengiraan yang tidak berakhir.

∞ (π): = 0 di mana π ∈ Π 0

∞ (φ?): = 0

∞ (α ∪ β): = ∞ (α) ∨ ∞ (β)

∞ (α; β): = ∞ (α) ∨ ∞ (β)

∞ (α *): = Δα ∨ ∞ (α)

Akhirnya, kebenaran keseluruhan program dapat dinyatakan melalui formula seumpamanya

A → (¬∞ (α) ∧ [α] B)

yang bermaksud secara harfiah bahawa jika A berlaku, maka program α tidak dapat berjalan selamanya dan setiap pelaksanaan yang berjaya akan berakhir dalam keadaan yang memuaskan B.

4. Beberapa varian

Hasil mengenai kekuatan ekspresi perbandingan, keraguan, kerumitan, aksiomatisasi dan kelengkapan sejumlah varian PDL yang diperoleh dengan memperluas atau membatasi sintaksnya dan semantiknya menjadi subjek kekayaan sastra. Kami hanya dapat mengatakan begitu banyak dan kami akan menangani beberapa varian ini yang meninggalkan sebahagian besar karya penting dalam logik dinamik.

4.1 PDL tanpa ujian

Skema aksioma [A?] B ↔ (A → B) nampaknya menunjukkan bahawa untuk setiap formula C, terdapat formula bebas ujian setara C '-ie, ada formula bebas ujian C' sehingga ⊨ C ↔ C '. Sangat menarik untuk diperhatikan bahawa pernyataan ini tidak benar. Biarkan PDL 0 menjadi batasan PDL untuk program biasa tanpa ujian, iaitu program yang tidak mengandungi ujian. Berman dan Paterson [1981] menganggap formula PDL <(p?; Π) *; ¬ p?; Π; p?> 1, yang manakah

< sambil p lakukan π> p

dan membuktikan bahawa tidak ada formula PDL 0 yang setara dengannya. Oleh itu, PDL mempunyai kekuatan yang lebih ekspresif daripada PDL 0. Hujah mereka sebenarnya dapat digeneralisasikan seperti berikut. Untuk semua n ≥ 0, biarkan PDL n +1 menjadi subset PDL di mana program boleh mengandungi ujian A? hanya jika A adalah formula n PDL. Untuk semua n ≥ 0, Berman dan Paterson menganggap formula PDL n +1 A n +1 yang ditentukan oleh

< sementara A n do π n > <π n > A n

di mana A 0  = p dan π 0  = π dan membuktikan bahawa untuk semua n ≥ 0, tidak ada formula PDL n yang setara dengan A n +1. Oleh itu, untuk semua n ≥ 0, PDL n +1 mempunyai daya ekspresif lebih banyak daripada PDL n.

4.2 PDL dengan sebaliknya

CPDL adalah peluasan PDL dengan sebaliknya. Ini adalah konstruk yang telah dipertimbangkan sejak awal PDL. Untuk semua program α, biarkan α -1 untuk program baru dengan semantik

x R (α -1) y iff y R (α) x.

Pembinaan sebaliknya memungkinkan kita untuk menyatakan fakta mengenai keadaan sebelum keadaan semasa dan membuat alasan mengenai program. Sebagai contoh, [α -1] A bermaksud bahawa sebelum melaksanakan α, A harus menahan. Kami ada

⊨ A → [α] <α -1 > A, ⊨ A → [α -1] A.

Penambahan konstruk sebaliknya tidak mengubah sifat PDL dengan cara yang ketara. Dengan menambahkan setiap contoh skema aksioma berikut:

(A8) A → [α] <α -1 > A

(A9) A → [α -1] A

kepada sistem bukti PDL, kami memperoleh predikat deducibility yang baik dan lengkap dalam bahasa yang diperluas. Lihat Parikh [1978] untuk perincian. CPDL mempunyai sifat model kecil dan (CPDL-SAT) lengkap SELESAI.

Sangat mudah untuk menyatakan bahawa CPDL mempunyai kekuatan yang lebih ekspresif daripada PDL. Untuk melihat ini, pertimbangkan formula CPDL <π -1 > 1 dan LTSs M = (W, R, V) dan M '= (W', R ', V') di mana W = {x, y}, R (π) = {(x, y)}, W '= {y'}, R '(π) = ∅ dan V (x) = V (y) = V' (y ') = ∅. Oleh kerana M, y sat <π -1 > 1, bukan M ', y' sat <π -1 > 1, dan kerana untuk semua formula PDL A, ini adalah M, y sat A iff M ', y' sat A, maka jelas bahawa tidak ada formula PDL yang setara dengan <π -1 > 1.

4.3 PDL dengan berulang dan gelung

Kami telah mengungkapkan kekuatan mengulangi di bahagian 3.3 dengan memperkenalkan RPDL. Di sini, kami meringkaskan lebih banyak hasil mengenai RPDL dan kaitannya dengan variasi lain mengenai konsep program berulang.

Mengenai teori kerumitan RPDL, Streett [1982] telah membuktikan bahawa RPDL mempunyai harta model terhingga; tepatnya bahawa setiap formula RPDL yang memenuhi syarat A dapat memenuhi syarat dalam model ukuran yang paling eksponensial tiga kali ganda pada panjang A. Argumen automatik-teori yang diizinkan untuk menyimpulkan bahawa masalah (RPDL-SAT) dapat diselesaikan dalam waktu eksponen triple deterministik (3-EKSPRESI). Jurang antara batas atas ini untuk memutuskan (RPDL-SAT) dan batas bawah masa eksponen mudah untuk membuat keputusan (PDL-SAT) telah terbuka. Masalahnya berkait rapat dengan minat saintis komputer yang semakin meningkat dalam mewujudkan kerumitan logik temporal, dan lebih khusus lagi mengenai (proposalional) mod μ-kalkulus (MMC) kerana Kozen [1983], kerana RPDL mempunyai pukulan linear- terjemahan ke MMC. Lebih-lebih lagi,Argumen Streett agak menetapkan preseden dalam penggunaan teknik automata yang kini meluas dalam membuktikan sifat komputasi logik program dan logik temporal. Dalam Vardi dan Stockmeyer [1985], batas atas dalam masa eksponen non-deterministik ditunjukkan. Dalam Emerson dan Jutla [1988] dan dalam bentuk terakhirnya di Emerson dan Jutla [1999], ditunjukkan bahawa (MMC-SAT) dan (RPDL-SAT) adalah LUAR BIASA-lengkap. Sekiranya kita menambah pengendali sebaliknya dari bahagian 4.2, seseorang akan memperoleh CRPDL. Kerumitan (CRPDL-SAT) tetap terbuka selama beberapa tahun tetapi ia juga boleh ditunjukkan dengan lengkap. Ini dicapai dengan menggabungkan teknik Emerson dan Jutla [1988] dan Vardi [1985], seperti di Vardi [1998]. Dalam Vardi dan Stockmeyer [1985], batas atas dalam masa eksponen non-deterministik ditunjukkan. Dalam Emerson dan Jutla [1988] dan dalam bentuk terakhirnya di Emerson dan Jutla [1999], ditunjukkan bahawa (MMC-SAT) dan (RPDL-SAT) adalah LUAR BIASA-lengkap. Sekiranya kita menambah pengendali sebaliknya dari bahagian 4.2, seseorang akan memperoleh CRPDL. Kerumitan (CRPDL-SAT) tetap terbuka selama beberapa tahun tetapi ia juga boleh ditunjukkan dengan lengkap. Ini dicapai dengan menggabungkan teknik Emerson dan Jutla [1988] dan Vardi [1985], seperti di Vardi [1998]. Dalam Vardi dan Stockmeyer [1985], batas atas dalam masa eksponen non-deterministik ditunjukkan. Dalam Emerson dan Jutla [1988] dan dalam bentuk terakhirnya di Emerson dan Jutla [1999], ditunjukkan bahawa (MMC-SAT) dan (RPDL-SAT) adalah LUAR BIASA-lengkap. Sekiranya kita menambah pengendali sebaliknya dari bahagian 4.2, seseorang akan memperoleh CRPDL. Kerumitan (CRPDL-SAT) tetap terbuka selama beberapa tahun tetapi ia juga boleh ditunjukkan dengan lengkap. Ini dicapai dengan menggabungkan teknik Emerson dan Jutla [1988] dan Vardi [1985], seperti di Vardi [1998]. Kerumitan (CRPDL-SAT) tetap terbuka selama beberapa tahun tetapi ia juga boleh ditunjukkan dengan lengkap. Ini dicapai dengan menggabungkan teknik Emerson dan Jutla [1988] dan Vardi [1985], seperti di Vardi [1998]. Kerumitan (CRPDL-SAT) tetap terbuka selama beberapa tahun tetapi ia juga boleh ditunjukkan dengan lengkap. Ini dicapai dengan menggabungkan teknik Emerson dan Jutla [1988] dan Vardi [1985], seperti di Vardi [1998].

Pada bahagian 3.3 kita telah mendefinisikan predikat ∞, di mana ∞ (α) bermaksud bahawa α dapat mempunyai perhitungan tidak berakhir. Kami memanggil LPDL logik yang diperoleh dengan menambahkan PDL dengan predikat ∞. Jelas, RPDL sekurang-kurangnya ekspresif seperti LPDL; Definisi induktif ∞ (α) dalam bahasa RPDL menyaksikannya. RPDL sebenarnya lebih ekspresif daripada LPDL. Ini ditunjukkan dalam Harel dan Sherman [1982]. Seperti yang disyaki, kedua-dua RPDL dan LPDL mempunyai kekuatan yang lebih ekspresif daripada PDL. Ini dibuktikan dengan membuktikan bahawa beberapa formula RPDL dan LPDL tidak mempunyai ungkapan yang setara dalam PDL. Pembuktiannya melibatkan teknik penyaringan yang dirancang untuk meruntuhkan LTS ke model terhingga sambil meninggalkan kebenaran atau kepalsuan formula tertentu. Untuk beberapa set formula PDL X,ia terdiri dalam pengelompokan ke kelas kesetaraan keadaan LTS yang memenuhi formula yang sama persis di X. Kumpulan kelas kesetaraan keadaan yang diperoleh sehingga menjadi set keadaan model filtrat, dan peralihan dibina dengan tepat di atasnya.

Dengan set FL (A) yang dipilih dengan teliti yang bergantung pada formula PDL A (yang disebut penutupan Fischer-Ladner dari set sub-formula A), penyaringan LTS M menghasilkan filtrat terhingga M ', seperti bahawa A dapat dipenuhi di dunia u di M jika dan hanya jika dapat memenuhi syarat di kelas kesetaraan yang mengandungi u di turasan. (Lihat Fischer dan Ladner [1979].)

Kita sekarang boleh mempertimbangkan penapisan LTS M = (W, R, V) di mana

  • W = {(i, j): j dan i bilangan bulat positif, 0 ≤ j ≤ i} ∪ {u}
  • (i, j) R (π) (i, j -1) apabila 1 ≤ j ≤ i
  • u R (π) (i, i) untuk setiap i
  • V (p) = ∅ untuk setiap p ∈ Φ 0

Dalam satu kalimat, apa yang berlaku di M adalah bahawa dari dunia u, terdapat sebilangan jalan π-tak terbatas yang semakin panjang. Kami mempunyai kedua-dua M, u sat ¬Δπ dan M, u sat ¬∞ (π *). Namun, untuk setiap formula PDL A, kita akan mempunyai Δπ dan ∞ (π *) yang berpuas hati pada kelas kesetaraan u dalam model yang diperoleh dengan penyaringan M dengan FL (A). Sesungguhnya, penapisan mesti meruntuhkan beberapa keadaan M dan membuat beberapa gelung. Oleh itu, tidak ada formula PDL yang dapat menyatakan Δπ atau ∞ (π *). namun, kita akan mempunyai Δπ dan ∞ (π *) yang berpuas hati pada kelas kesetaraan u dalam sebarang filtrat terhingga M. Oleh itu, Δπ dan ∞ (π *) tidak dapat dinyatakan dalam PDL.

Terdapat cara lain untuk memungkinkan penegasan bahawa program dapat dilaksanakan selama-lamanya. Sebagai contoh, Danecki [1984a] mencadangkan sloop predikat untuk memenuhi syarat program yang dapat masuk dalam gelung kuat, iaitu:

V (sloop (α)) = {x: x R (α) x}

Mari kita panggil SLPDL logik yang diperoleh dengan menambah PDL dengan sloop (α). RPDL dan SLPDL pada dasarnya tidak dapat dibandingkan: predikat Δ tidak dapat ditentukan dalam SLPDL, dan predikat sloop tidak dapat ditentukan dalam RPDL. SLPDL tidak memiliki harta model terhingga. Contohnya, formula

[π *] (1 ¬ sloop+))

cukup memuaskan hanya dalam LTS yang tidak terhingga. Walaupun demikian, Danecki [1984a] menetapkan kebolehtentuan formula (SLPDL-SAT) dalam masa eksponen deterministik.

4.4 PDL dengan persimpangan

Konstruk lain telah dikaji: persimpangan program. Dengan menambahkan persimpangan program ke PDL, kita memperoleh logik IPDL. Di IPDL, untuk semua program α, β, ungkapan α∩β bermaksud program baru dengan semantik

x R (α∩β) y iff x R (α) y dan x R (β) y

Sebagai contoh, pembacaan A yang dimaksudkan adalah bahawa jika kita menjalankan α dan β dalam keadaan sekarang maka ada keadaan yang dapat dicapai oleh kedua program yang memenuhi A. Hasilnya, kita mempunyai

⊨ A → A ∧ A

tetapi, secara amnya, kita ada

bukan ⊨ A ∧ A → A

Walaupun persimpangan program memainkan peranan penting dalam pelbagai aplikasi PDL untuk kecerdasan buatan dan sains komputer, teori bukti dan teori kerumitan PDL dengan persimpangan tetap tidak dapat diterokai selama beberapa tahun. Mengenai teori kerumitan IPDL, kesulitan muncul ketika seseorang mempertimbangkan harta model terhingga. Sebenarnya konstruk sloop (α) dapat dinyatakan dalam IPDL. Dalam logik dinamik proporsional dengan persimpangan, ia setara dengan 1. Oleh itu, kita dapat menyesuaikan formula IPDL bahagian 4.3, dan kita mempunyai

[π *] (1 ∧ [π + ∩1?] 0)

cukup memuaskan hanya dalam LTS yang tidak terhingga. Dengan kata lain, IPDL tidak memiliki harta model terhingga. Danecki [1984b] menyelidiki teori kerumitan IPDL dan menunjukkan bahawa membuat keputusan (IPDL-SAT) dapat dilakukan dalam masa eksponen berganda deterministik. (Bukti moden dikemukakan dalam Göller, Lohrey dan Lutz [2007].) Jurang kerumitan antara batas atas masa eksponen dua ini untuk membuat keputusan (IPDL-SAT) dan batas bawah masa eksponen mudah untuk membuat keputusan (PDL-SAT) yang diperoleh oleh Fischer dan Ladner [1979] tetap terbuka selama lebih dari dua puluh tahun. Pada tahun 2004, Lange [2005] menetapkan batas bawah ruang eksponensial (IPDL-SAT). Pada tahun 2006,Lange dan Lutz [2005] memberikan bukti had bawah eksponensial-ganda dari masalah kepuasan untuk IPDL tanpa ujian dengan pengurangan dari masalah perkataan mesin Turing berselang-seli dengan ruang yang eksponensial. Dalam pengurangan ini, peranan konstruksi iterasi sangat penting kerana, menurut Massacci [2001], masalah kepuasan untuk IPDL tanpa lelaran tanpa ujian hanya lengkap PSPACE. Menambah konstruk sebaliknya ke IPDL, kami memperoleh ICPDL. Masalah kepuasan ICPDL telah terbukti menjadi 2-EXPTIME-lengkap oleh Göller, Lohrey dan Lutz [2007]. Masalah kepuasan ICPDL telah terbukti menjadi 2-EXPTIME-lengkap oleh Göller, Lohrey dan Lutz [2007]. Masalah kepuasan ICPDL telah terbukti menjadi 2-EXPTIME-lengkap oleh Göller, Lohrey dan Lutz [2007].

Mengenai teori bukti IPDL, kesulitan muncul ketika kita menyedari bahawa tidak ada skema aksioma, dalam bahasa PDL dengan persimpangan, "sesuai" dengan semantik x R (α∩β) y iff x R (α) y dan x R (β) y program α∩β. Iaitu, tidak dengan cara yang sama misalnya, bahawa skema aksioma (A1) dan (A2) masing-masing "sesuai" dengan semantik program α; β dan α∪β. Atas sebab ini, aksiomatisasi PDL dengan persimpangan dibuka sehingga sistem bukti lengkap dikembangkan di Balbiani dan Vakarelov [2003].

Dalam varian lain dari PDL, kerana Peleg [1987] dan selanjutnya dikaji oleh Goldblatt [1992b], ungkapan α∩β ditafsirkan "do α dan β secara selari". Dalam konteks ini, hubungan binari R (α) dan R (β) bukan lagi kumpulan pasangan bentuk (x, y) dengan dunia x, y, melainkan set pasangan bentuk (x, Y) dengan xa dunia dan Y satu set dunia. Itu terinspirasi oleh Game Logic of Parikh [1985], intepretasi PDL dengan "program sebagai permainan". Game Logic menyediakan konstruk program tambahan yang menggandakan program, sehingga memungkinkan untuk menentukan persimpangan program sebagai dua pilihan non-deterministik antara program.

5. Kesimpulan

Artikel ini telah memfokuskan pada logik dinamik cadangan dan beberapa variannya yang signifikan. Kini terdapat sejumlah buku-Goldblatt [1982], Goldblatt [1992a], Harel [1979] dan Harel, Kozen dan Tiuryn [2000] -dan makalah tinjauan-Harel [1984], Kozen dan Tiuryn [1990], Parikh [1983] -mengubati PDL dan formalisme yang berkaitan. Badan penyelidikan PDL tentunya berperanan dalam mengembangkan banyak teori logik mengenai dinamika sistem. Walau bagaimanapun, teori-teori ini boleh dikatakan tidak termasuk dalam ruang lingkup artikel ini. Van Eijck dan Stokhof [2006] adalah gambaran keseluruhan topik yang menggunakan logik dinamik, menangani pelbagai tema yang menarik minat para ahli falsafah: misalnya, dinamika komunikasi, atau semantik bahasa semula jadi. Buku-buku terkini memuat banyak maklumat mengenai topik yang lebih baru,seperti logik pengetahuan dinamik (logik epistemik dinamik) dalam Van Ditmarsch, Van Der Hoek dan Kooi [2007], dan logik dinamik sistem berterusan dan hibrid (logik dinamik pembezaan) di Platzer [2010]. PDL dirancang terutamanya untuk membuat pertimbangan mengenai program. Terdapat banyak aplikasi logik modal untuk penaakulan mengenai program. Logik algoritma lebih dekat dengan PDL kerana membolehkan seseorang bercakap secara jelas mengenai program. Pembaca dijemput untuk meninjau karya yang dikaji di Mirkowska dan Salwicki [1987]. Logik sementara kini menjadi logik utama dalam sains komputer teori dan mempunyai kaitan rapat dengan logik program. Mereka membenarkan seseorang untuk mengekspresikan tingkah laku sementara sistem peralihan dengan bahasa yang menjauhkan diri dari label (oleh itu program). Lihat misalnya Schneider [2004] untuk gambaran keseluruhan asas dalam bidang penyelidikan ini.

Bibliografi

  • Apt, K., 1981, “Sepuluh tahun logik Hoare: Satu tinjauan - Bahagian I”, Transaksi ACM pada Bahasa dan Sistem Pengaturcaraan, 3 (4): 431–483.
  • Balbiani, P., dan D. Vakarelov, 2003, "PDL dengan persimpangan program: aksiomatisasi lengkap", Jurnal Logik Non-Klasik Terapan, 13: 231-276.
  • van Benthem, J., 1998, “Pembinaan program yang selamat untuk bisimulasi”, Studia Logica, 60: 311–330.
  • Berman, F., dan M. Paterson, 1981, "Logik dinamik cadangan lebih lemah tanpa ujian", Sains Komputer Teoretikal, 16: 321-328.
  • Burstall, R., 1974, “Program Proving as Hand Simulation with a Little Induction”, Pemprosesan Maklumat 74: Prosiding IFIP Congress 74, Amsterdam: North Holland Publishing Company, 308–312.
  • Danecki, R., 1984a, "Logik dinamik cadangan dengan predikat gelung kuat", dalam M. Chytil dan V. Koubek, Matematik Asas Sains Komputer, Berlin: Springer-Verlag, 573-581.
  • –––, 1984b, “Logik dinamik proposisional yang tidak dapat ditentukan dengan persimpangan dapat ditentukan”, dalam A. Skowron (ed.), Teori Pengiraan, Berlin: Springer-Verlag, 34-53.
  • De Giacomo, G., dan F. Massacci, 2000, "Menggabungkan pemotongan dan pemeriksaan model ke dalam tableaux dan algoritma untuk PDL sebaliknya", Maklumat dan Pengiraan, 160: 109–169.
  • van Ditmarsch, H., W. van Der Hoek, dan B. Kooi, 2007, Logik epistemik dinamik, Dordrecht: Springer-Verlag.
  • van Eijck, J., dan M. Stokhof, 2006, "The Gamut of Dynamic Logics", dalam D. Gabbay dan J. Woods (eds.), Buku Panduan Sejarah Logik, Jilid 7- Logik dan Modaliti dalam Twentieth Century, Amsterdam: Elsevier, 499-600.
  • Emerson, E., dan Jutla, C., 1988, "Kompleksitas Automata Pohon dan Logik Program (Abstrak yang Diperpanjang)", dalam Prosiding Simposium Tahunan ke-29 mengenai Asas Sains Komputer, Los Alamitos, CA: Persatuan Komputer Komputer IEEE, 328–337.
  • –––, 1999, “Kompleksitas Automata Pohon dan Logik Program”, dalam SIAM Journal of Computing, 29: 132–158.
  • Engeler, E., 1967, "Algoritma sifat struktur", Teori Sistem Matematik, 1: 183–195.
  • Fischer, M., dan R. Ladner, 1979, “Logik dinamik cadangan program biasa”, Jurnal Sains Komputer dan Sistem, 18: 194–211.
  • Floyd, R., 1967, "Menetapkan makna untuk program", Prosiding Simposium Masyarakat Matematik Amerika mengenai Matematik Terapan (Jilid 19), Providence, RI: Persatuan Matematik Amerika, 19-31.
  • Gargov, G., dan S. Passy, 1988, "Determinisme dan perulangan dalam PDL gabungan", Sains Komputer Teoritis, Amsterdam: Elsevier, 259–277.
  • Goldblatt, R., 1982, Axiomatising the Logic of Computer Programming, Berlin: Springer-Verlag.
  • –––, 1992a, Logik Masa dan Pengiraan, Stanford: Pusat Pengajian Bahasa dan Penerbitan Maklumat.
  • –––, 1992b, “Tindakan Selari: Logik Dinamik Serentak dengan Modaliti Bebas”, Studia Logica, 51: 551–578.
  • Göller, S., M. Lohrey, dan C. Lutz, 2007, "PDL dengan persimpangan dan pembalikan adalah 2EXP-lengkap", Yayasan Sains Perisian dan Struktur Komputasi, Berlin: Springer, 198-212.
  • Harel, D., 1979, Logik Dinamik Tertib Pertama, Berlin: Springer-Verlag.
  • –––, 1983, “Domino berulang: membuat yang sangat tidak dapat dikira sangat dapat dipahami”, dalam M. Karpinski (ed.), Foundations of Computation Theory, Berlin: Springer-Verlag, 177–194.
  • –––, 1984, “Logik dinamik”, dalam D. Gabbay dan F. Guenthner (ed.), Buku Panduan Logik Falsafah (Jilid II), Dordrecht: D. Reidel, 497–604.
  • Harel, D., D. Kozen, dan J. Tiuryn, 2000, Dynamic Logic, Cambridge, MA: MIT Press.
  • Harel, D. dan Sherman, R., 1982, “Looping vs. Repeating in Dynamic Logic”, Maklumat dan Kawalan, 55: 175–192.
  • Hoare, C., 1969, "Dasar aksiomatik untuk pengaturcaraan komputer", Komunikasi Persatuan Mesin Pengkomputeran, 12: 576-580.
  • Kozen, D., 1983, "Hasil pada Proposalional μ-Kalkulus", Sains Komputer Teoritis, 27: 333-354.
  • Kozen, D., dan R. Parikh, 1981, "Bukti dasar kelengkapan PDL", Sains Komputer Teoritis, 14: 113–118.
  • Kozen, D., dan J. Tiuryn, 1990, "Logik program", dalam J. Van Leeuwen (ed.), Buku Panduan Ilmu Komputer Teoritis (Jilid B), Amsterdam: Elsevier, 789-840.
  • Lange, M., 2005, "Kerumitan yang lebih rendah terikat untuk logik dinamik proposisional dengan persimpangan", dalam R. Schmidt, I. Pratt-Hartmann, M. Reynolds dan H. Wansing (eds.), Kemajuan dalam Logik Modal (Jilid 5), London: King's College Publications, 133–147.
  • Lange, M., dan C. Lutz, 2005, "2-EXPTIME batas bawah untuk logik dinamik proposisi dengan persimpangan", Jurnal Logik Simbolik, 70: 1072-1086.
  • Lutz, C., 2005, "PDL dengan persimpangan dan sebaliknya adalah sukar diputuskan". Dalam L. Ong (ed.), Logik Sains Komputer, Berlin: Springer-Verlag, 413-427.
  • Massacci, F., 2001, "Prosedur keputusan untuk logik deskripsi ekspresif dengan persimpangan, komposisi, pembalikan peranan dan identiti peranan", dalam B. Nebel (ed.), Persidangan Bersama Antarabangsa ke-17 mengenai Artificial Intelligence, San Francisco: Morgan Kaufmann, 193–198.
  • Mirkowska, G., dan A. Salwicki, 1987, Algoritma Logik, Dordrecht: D. Reidel.
  • Nishimura, H., 1979, "Kaedah berurutan dalam logika dinamik proposisional", Acta Informatica, 12: 377–400.
  • Parikh, R., 1978, "Kelengkapan logika dinamis proposisional", dalam J. Winkowski (ed.), Asas Matematik Sains Komputer, Berlin: Springer-Verlag, 1978, 403-415.
  • –––, 1983, “Logik cadangan program: arahan baru”, dalam M. Karpinski (ed.), Asas Teori Pengiraan, Berlin: Springer-Verlag, 347-359.
  • –––, 1985, “Logik permainan dan aplikasinya”, Annals of Discrete Mathematics, 24: 111–140.
  • Peleg, D., 1987, “Logik dinamik serentak”, Jurnal Persatuan Mesin Pengkomputeran, 34: 450–479.
  • Platzer, A., 2010, Analisis Logik Sistem Hibrid: Membekalkan Teorema untuk Dinamika Kompleks, Berlin: Springer, 2010.
  • Pratt, V., 1976, “Pertimbangan semantik mengenai logik Floyd-Hoare”, dalam Prosiding Simposium IEEE ke-17 mengenai Asas Sains Komputer, Los Alamitos, CA: Persatuan Komputer Komputer IEEE, 109–121.
  • –––, 1978, “Kaedah keputusan praktikal untuk logik dinamik proposional”, dalam Prosiding Simposium ACM Tahunan ke-10 mengenai Teori Pengkomputeran, New York, NY: ACM, 326–337.
  • –––, 1980a, “Kaedah yang hampir optimum untuk menaakul tindakan”, Jurnal Sains Komputer dan Sistem, 20: 231–254.
  • –––, 1980b, “Aplikasi Logik Modal untuk Pengaturcaraan”, Studia Logica, 39: 257–274.
  • Sakalauskaite, J., dan M. Valiev, 1990, "Kelengkapan logika dinamis proposisi dengan pengulangan tak terhingga", dalam P. Petkov (ed.), Logika Matematik, New York: Plenum Press, 339–349.
  • Salwicki, A., 1970, "Bahasa algoritma formal", Buletin de l'Academie Polonaise des Sciences, Serie des science mathematiques, astronomiques et physiques, 18: 227-232.
  • Segerberg, K., 1977, "Teoritas kelengkapan dalam logika modal program", Notis Persatuan Matematik Amerika, 24: 522.
  • Schneider, K., 2004, Pengesahan Sistem Reaktif, Berlin: Springer-Verlag.
  • Streett, R., 1982, "Logik dinamik cadangan perulangan dan pembalikan adalah dasar yang dapat ditentukan", Maklumat dan Pengendalian, 54: 121–141.
  • Vakarelov, D., 1983, "Teorema penapisan untuk algebra dinamik dengan ujian dan pengendali songsang", dalam A. Salwicki (ed.), Logik Program dan Aplikasi mereka, Berlin: Springer-Verlag, 314–324.
  • Vardi, M., 1985, "Taming of Converse: Reasoning about Two-way Computations", dalam Nota Kuliah dalam Sains Komputer (Jilid 193), Berlin-Heidelberg: Springer, 413-423.
  • –––, 1998, “Berpikir tentang masa lalu dengan automata dua arah”, dalam Nota Kuliah dalam Sains Komputer (Jilid 1443), Berlin-Heidelberg: Springer, 628–641.
  • Vardi, M., dan Stockmeyer, L., 1985, "Peningkatan Batas Atas dan Bawah untuk Logik Modal Program: Laporan Awal", dalam Prosiding Simposium ACM Tahunan ke-17 pada Teori Pengkomputeran, New York, NY: ACM, 240 –251.
  • Yanov, J., 1959, “Tentang kesetaraan skema pengendali”, Masalah Cybernetic, 1: 1–100.

Alat Akademik

ikon sep lelaki
ikon sep lelaki
Cara memetik entri ini.
ikon sep lelaki
ikon sep lelaki
Pratonton versi PDF entri ini di Friends of the SEP Society.
ikon inpho
ikon inpho
Cari topik entri ini di Projek Ontologi Falsafah Internet (InPhO).
ikon kertas phil
ikon kertas phil
Bibliografi yang dipertingkatkan untuk entri ini di PhilPapers, dengan pautan ke pangkalan data.

Sumber Internet Lain

[Sila hubungi pengarang dengan cadangan.]

Disyorkan: