Apa perbedaan antara LTL dan CTL?

Saya sudah membaca contoh formula dalam CTL tetapi tidak dalam LTL dan sebaliknya, tapi saya mengalami kesulitan untuk mendapatkan pemahaman mental tentang formula LTL dan sebenarnya apa, pada intinya, bedanya.

Untuk benar-benar memahami perbedaan antara LTL dan CTL Anda harus mempelajari semantik kedua bahasa. Rumus LTL menunjukkan properti yang akan ditafsirkan pada setiap pelaksanaan program. Untuk setiap kemungkinan eksekusi (pelarian), yang dapat dilihat sebagai urutan peristiwa atau status pada suatu garis - dan inilah mengapa ia dinamakan "waktu linier" - kepuasan diperiksa pada pelarian tanpa kemungkinan beralih ke pelarian lainnya selama pemeriksaan. Di sisi lain, semantik CTL memeriksa rumus pada semua kemungkinan yang berjalan dan akan mencoba semua kemungkinan yang berjalan ( operator A ) atau hanya satu yang berjalan ( operator E ) ketika menghadapi cabang.

Dalam praktiknya ini berarti bahwa beberapa formula dari setiap bahasa tidak dapat dinyatakan dalam bahasa lain. Sebagai contoh, properti reset (properti reachability penting untuk desain sirkuit) menyatakan bahwa selalu ada kemungkinan bahwa keadaan dapat dicapai selama menjalankan, bahkan jika itu tidak pernah benar-benar tercapai ( AG EF reset ). LTL hanya dapat menyatakan bahwa kondisi reset sebenarnya telah tercapai dan tidak dapat dicapai.

Di sisi lain, rumus LTL tidak dapat diterjemahkan ke dalam CTL. Formula ini menunjukkan properti stabilitas: dalam setiap pelaksanaan program, s akhirnya akan benar sampai akhir program (atau selamanya jika program tidak pernah berhenti). CTL hanya dapat memberikan formula yang terlalu ketat ( AG AG ) atau terlalu permisif ( AF EG ). Yang kedua jelas salah. Tidak begitu mudah untuk yang pertama. Namun AF AG salah. Pertimbangkan sebuah sistem yang loop pada A1 , bisa pergi dari A1 ke B dan kemudian akan pergi ke A2$\Diamond\Box s$pada langkah selanjutnya. Maka sistem akan tetap dalam keadaan A2 selamanya. Kemudian "sistem akhirnya akan tetap dalam keadaan A " adalah properti dari tipe . Jelas bahwa properti ini berlaku pada sistem. Namun, AF AG s bisa tidak menangkap properti ini sejak sebaliknya adalah benar: ada lari di mana sistem akan selalu berada dalam keadaan yang lari akhirnya pergi di non A negara.$\Diamond\Box s$

Saya tidak tahu apakah ini menjawab pertanyaan Anda, tetapi saya ingin menambahkan beberapa komentar.

Ada banyak diskusi tentang logika terbaik untuk mengekspresikan properti untuk verifikasi perangkat lunak ... tetapi perdebatan sebenarnya ada di tempat lain. LTL dapat mengekspresikan properti penting untuk pemodelan sistem perangkat lunak (keadilan) ketika CTL harus memiliki semantik baru (hubungan kepuasan baru) untuk mengekspresikannya. Tetapi algoritma CTL biasanya lebih efisien dan dapat menggunakan algoritma berbasis BDD. Jadi ... tidak ada solusi terbaik. Hanya dua pendekatan yang berbeda, sejauh ini.

Salah satu komentator menyarankan makalah Vardi "Branching versus Linear Time: Final Showdown" .

Jika diberikan satu objek (misalnya jejak dalam kasus LTL), Anda hanya mempertimbangkan satu masa depan untuk setiap titik waktu, dalam CTL Anda memiliki sejumlah besar objek tersebut.

Secara khusus, nextmemberikan tindakan unik dalam LTL tetapi (berpotensi) seluruh set dalam CTL.