Logika Temporal Linier (Linear-Time Temporal Logic, LTL)

Logika Temporal Linier (Linear-Time Temporal Logic, LTL) Kuliah (Pengantar) Metode Formal Semester Ganjil 2015-2016

M. Arzaki Fakultas Informatika Telkom University FIF Tel-U

November 2015

MZI (FIF Tel-U)

LTL

November 2015

1 / 74

Acknowledgements

Slide ini disusun berdasarkan materi yang terdapat pada sumber-sumber berikut: Buku: 1

Logic in Computer Science: Modelling and Reasoning about Systems, Edisi 2, 2004, oleh M. Huth dan M. Ryan (acuan utama).

2

Mathematical Logic for Computer Science, Edisi 2, 2000, oleh M. Ben-Ari.

3

Practical Formal Methods Using Temporal Logics, 2011, oleh Michael Fischer.

MZI (FIF Tel-U)

LTL

November 2015

2 / 74

Slide kuliah: 1

Slide kuliah Metode Formal dan Topik dalam Logika Komputasional di Fasilkom UI oleh B. H. Widjaja.

2

Slide kuliah Metode Formal di University of Bozen-Bolzano oleh Enrico Franconi.

3

Slide kuliah Metode Formal dari Veri…ed Software Systems.

4

Slide kuliah Introduction to Computational Logic di Academia Sinica oleh Bow-Yaw Wang.

5

Slide kuliah Linear Temporal Logic di California Institute of Technology oleh Richard M. Murray.

6

Slide kuliah Linear and Branching Temporal Logics di Radboud University Nijmegen oleh Frits Vaandrager. Beberapa slide kuliah lain.

7

Beberapa gambar dapat diambil dari sumber-sumber di atas. Slide ini ditujukan untuk keperluan akademis di lingkungan FIF Telkom University. Jika Anda memiliki saran/ pendapat/ pertanyaan terkait materi dalam slide ini, silakan kirim email ke @telkomuniversity.ac.id. MZI (FIF Tel-U)

LTL

November 2015

3 / 74

Bahasan 1

Logika Temporal: Pendahuluan dan Motivasi

2

Pemodelan Waktu pada LTL

3

Operator Temporal dan Makna Intuitifnya

4

Sintaks Formal LTL

5

Semantik Formal LTL

6

LTL untuk Spesi…kasi Sistem Reaktif

7

Formula LTL Berdasarkan Semantiknya

8

Contoh Pemodelan Sederhana dengan LTL

9

Keterkaitan LTL dengan Logika Predikat dan Keterputusan untuk LTL

MZI (FIF Tel-U)

LTL

November 2015

4 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

5 / 74

Pendahuluan dan Motivasi Dalam logika klasik – contohnya logika proposisi yang telah kita pelajari di awal perkuliahan – nilai kebenaran formula dievaluasi dalam suatu “dunia yang tetap” (…xed world). Contohnya, proposisi: “hari ini adalah hari Senin” hanya dapat bernilai benar (true/ T) atau salah (false/ F), tetapi tidak keduanya. Nilai kebenaran proposisi tersebut juga tetap (konstan).

MZI (FIF Tel-U)

LTL

November 2015

6 / 74

Pendahuluan dan Motivasi Dalam logika klasik – contohnya logika proposisi yang telah kita pelajari di awal perkuliahan – nilai kebenaran formula dievaluasi dalam suatu “dunia yang tetap” (…xed world). Contohnya, proposisi: “hari ini adalah hari Senin” hanya dapat bernilai benar (true/ T) atau salah (false/ F), tetapi tidak keduanya. Nilai kebenaran proposisi tersebut juga tetap (konstan). Logika proposisi saja tidak cukup untuk memodelkan dan mengekspresikan proses pada suatu sistem yang dinamis (bukan hanya sistem komputasional). Mengapa kita tidak memakai logika predikat?

MZI (FIF Tel-U)

LTL

November 2015

6 / 74

Pendahuluan dan Motivasi Dalam logika klasik – contohnya logika proposisi yang telah kita pelajari di awal perkuliahan – nilai kebenaran formula dievaluasi dalam suatu “dunia yang tetap” (…xed world). Contohnya, proposisi: “hari ini adalah hari Senin” hanya dapat bernilai benar (true/ T) atau salah (false/ F), tetapi tidak keduanya. Nilai kebenaran proposisi tersebut juga tetap (konstan). Logika proposisi saja tidak cukup untuk memodelkan dan mengekspresikan proses pada suatu sistem yang dinamis (bukan hanya sistem komputasional). Mengapa kita tidak memakai logika predikat? Ingat kembali bahwa secara umum masalah satis…ability (keterpenuhan) pada logika predikat adalah masalah yang bersifat undecidable (tak terputuskan).

MZI (FIF Tel-U)

LTL

November 2015

6 / 74

Pendahuluan dan Motivasi Dalam logika klasik – contohnya logika proposisi yang telah kita pelajari di awal perkuliahan – nilai kebenaran formula dievaluasi dalam suatu “dunia yang tetap” (…xed world). Contohnya, proposisi: “hari ini adalah hari Senin” hanya dapat bernilai benar (true/ T) atau salah (false/ F), tetapi tidak keduanya. Nilai kebenaran proposisi tersebut juga tetap (konstan). Logika proposisi saja tidak cukup untuk memodelkan dan mengekspresikan proses pada suatu sistem yang dinamis (bukan hanya sistem komputasional). Mengapa kita tidak memakai logika predikat? Ingat kembali bahwa secara umum masalah satis…ability (keterpenuhan) pada logika predikat adalah masalah yang bersifat undecidable (tak terputuskan). Dalam logika temporal, nilai kebenaran suatu formula dievaluasi dalam “suatu himpunan dunia” (set of worlds), akibatnya suatu formula yang menyatakan “hari ini adalah hari Senin” dapat dipenuhi di suatu dunia, tetapi tidak dipenuhi pada dunia yang lain. “Dunia” yang dimaksud di sini terkait dengan waktu (temporal). MZI (FIF Tel-U)

LTL

November 2015

6 / 74

Bagaimana cara kita berpindah dari satu dunia ke dunia lain bergantung pada cara kita melihat keterkaitan antar waktu.

MZI (FIF Tel-U)

LTL

November 2015

7 / 74

Bagaimana cara kita berpindah dari satu dunia ke dunia lain bergantung pada cara kita melihat keterkaitan antar waktu. Waktu akan dimodelkan dengan accessibility relation antar dunia. Logika temporal memperluas gagasan pada logika proposisi dengan menambahkan operator temporal (temporal operators) yang diperlukan untuk berpindah dari satu dunia ke dunia lain. Pemodelan waktu pada logika temporal dapat berupa:

MZI (FIF Tel-U)

LTL

November 2015

7 / 74

Bagaimana cara kita berpindah dari satu dunia ke dunia lain bergantung pada cara kita melihat keterkaitan antar waktu. Waktu akan dimodelkan dengan accessibility relation antar dunia. Logika temporal memperluas gagasan pada logika proposisi dengan menambahkan operator temporal (temporal operators) yang diperlukan untuk berpindah dari satu dunia ke dunia lain. Pemodelan waktu pada logika temporal dapat berupa: 1 pemodelan waktu-linier (linear-time) atau waktu-bercabang (branching-time): waktu-linier biasanya dipakai untuk memodelkan sistem deterministik, sedangkan waktu-bercabang biasanya dipakai untuk memodelkan sistem non-deterministik.

MZI (FIF Tel-U)

LTL

November 2015

7 / 74

Bagaimana cara kita berpindah dari satu dunia ke dunia lain bergantung pada cara kita melihat keterkaitan antar waktu. Waktu akan dimodelkan dengan accessibility relation antar dunia. Logika temporal memperluas gagasan pada logika proposisi dengan menambahkan operator temporal (temporal operators) yang diperlukan untuk berpindah dari satu dunia ke dunia lain. Pemodelan waktu pada logika temporal dapat berupa: 1 pemodelan waktu-linier (linear-time) atau waktu-bercabang (branching-time): waktu-linier biasanya dipakai untuk memodelkan sistem deterministik, sedangkan waktu-bercabang biasanya dipakai untuk memodelkan sistem non-deterministik. 2 pemodelan waktu-kontinu (continuous-time) atau waktu-diskret (discrete-time): waktu-kontinu biasanya dipakai pada komputer analog atau pada sistem yang terkait dengan sistem waktu-nyata (real-time system) yang memerlukan presisi tinggi terkait waktu, sedangkan waktu-diskret biasanya dipakai pada sistem yang tidak memerlukan pengawasan secara kontinu terus menerus atau presisi terkait waktunya agak longgar.

MZI (FIF Tel-U)

LTL

November 2015

7 / 74

Bagaimana cara kita berpindah dari satu dunia ke dunia lain bergantung pada cara kita melihat keterkaitan antar waktu. Waktu akan dimodelkan dengan accessibility relation antar dunia. Logika temporal memperluas gagasan pada logika proposisi dengan menambahkan operator temporal (temporal operators) yang diperlukan untuk berpindah dari satu dunia ke dunia lain. Pemodelan waktu pada logika temporal dapat berupa: 1 pemodelan waktu-linier (linear-time) atau waktu-bercabang (branching-time): waktu-linier biasanya dipakai untuk memodelkan sistem deterministik, sedangkan waktu-bercabang biasanya dipakai untuk memodelkan sistem non-deterministik. 2 pemodelan waktu-kontinu (continuous-time) atau waktu-diskret (discrete-time): waktu-kontinu biasanya dipakai pada komputer analog atau pada sistem yang terkait dengan sistem waktu-nyata (real-time system) yang memerlukan presisi tinggi terkait waktu, sedangkan waktu-diskret biasanya dipakai pada sistem yang tidak memerlukan pengawasan secara kontinu terus menerus atau presisi terkait waktunya agak longgar. Logika temporal linier (linear-time temporal logic/ linear temporal logic, LTL) adalah suatu kerangka logika yang dapat dipakai untuk memodelkan suatu sistem dengan model waktu-linier dan bersifat diskrit. Salah satu sistem sederhana yang dapat dimodelkan dengan LTL adalah lampu lalu lintas jalan (tra¢ c light). MZI (FIF Tel-U)

LTL

November 2015

7 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

8 / 74

Pemodelan Waktu pada LTL Pada LTL, waktu dimodelkan secara diskrit dan linier.

Pada gambar di atas, 0; 1; 2; 3; : : : merepresentasikan state pada LTL. Secara umum, model waktu untuk LTL akan serupa (isomor…k) dengan himpunan bilangan asli N.

Catatan Untuk meringkas penulisan, kita akan menotasikan himpunan f0; 1; 2; : : :g dengan N0 dan himpunan f1; 2; 3; : : :g dengan N.

MZI (FIF Tel-U)

LTL

November 2015

9 / 74

Pandang ilustrasi berikut:

Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0;

MZI (FIF Tel-U)

LTL

November 2015

10 / 74


Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0; 7;

MZI (FIF Tel-U)

LTL

November 2015

10 / 74


Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0; 7; 14; : : :, atau secara umum pada state ke-

MZI (FIF Tel-U)

LTL

November 2015

10 / 74


Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0; 7; 14; : : :, atau secara umum pada state ke-7k, k 2 N0 T uesday bernilai T pada state 1;

MZI (FIF Tel-U)

LTL

November 2015

10 / 74


Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0; 7; 14; : : :, atau secara umum pada state ke-7k, k 2 N0 T uesday bernilai T pada state 1; 8;

MZI (FIF Tel-U)

LTL

November 2015

10 / 74


Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0; 7; 14; : : :, atau secara umum pada state ke-7k, k 2 N0

T uesday bernilai T pada state 1; 8; 15; : : :, atau secara umum pada state ke-

MZI (FIF Tel-U)

LTL

November 2015

10 / 74


Misalkan terdapat himpunan proposisi P = fM onday; T uesday; : : : ; Sundayg dan himpunan state S = f0; 1; 2; : : :g, kita memiliki: M onday bernilai T pada state 0; 7; 14; : : :, atau secara umum pada state ke-7k, k 2 N0

T uesday bernilai T pada state 1; 8; 15; : : :, atau secara umum pada state ke-7k + 1, k 2 N0 dan seterusnya.

MZI (FIF Tel-U)

LTL

November 2015

10 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

11 / 74


Operator temporal pada LTL terdiri dari: operator uner: X; F; G operator biner: U; W; R

MZI (FIF Tel-U)

LTL

November 2015

12 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X :

benar pada state berikutnya,

MZI (FIF Tel-U)

LTL

November 2015

13 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X : benar pada state berikutnya, is true in the neXt moment of time. Operator X disebut dengan operator next atau operator “X” F :

benar pada suatu state (saat ini atau suatu state berikutnya),

MZI (FIF Tel-U)

LTL

November 2015

13 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X : benar pada state berikutnya, is true in the neXt moment of time. Operator X disebut dengan operator next atau operator “X” F : benar pada suatu state (saat ini atau suatu state berikutnya), is true in the Future (or present) moment of time atau is Finally true. Operator F disebut dengan operator future atau operator “F”. G :

benar pada semua state (saat ini dan semua state berikutnya),

MZI (FIF Tel-U)

LTL

November 2015

13 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X : benar pada state berikutnya, is true in the neXt moment of time. Operator X disebut dengan operator next atau operator “X” F : benar pada suatu state (saat ini atau suatu state berikutnya), is true in the Future (or present) moment of time atau is Finally true. Operator F disebut dengan operator future atau operator “F”. G : benar pada semua state (saat ini dan semua state berikutnya), holds Globally in the moment of time. Operator G disebut dengan operator global atau operator “G”. U :

benar hingga suatu state ketika

MZI (FIF Tel-U)

LTL

benar,

November 2015

13 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X : benar pada state berikutnya, is true in the neXt moment of time. Operator X disebut dengan operator next atau operator “X” F : benar pada suatu state (saat ini atau suatu state berikutnya), is true in the Future (or present) moment of time atau is Finally true. Operator F disebut dengan operator future atau operator “F”. G : benar pada semua state (saat ini dan semua state berikutnya), holds Globally in the moment of time. Operator G disebut dengan operator global atau operator “G”. U : benar hingga suatu state ketika benar, is true Until some future moment when is true. Operator U disebut dengan operator until atau operator “U”. W :

akan selalu benar, kecuali bila

MZI (FIF Tel-U)

LTL

benar maka

boleh tidak benar

November 2015

13 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X : benar pada state berikutnya, is true in the neXt moment of time. Operator X disebut dengan operator next atau operator “X” F : benar pada suatu state (saat ini atau suatu state berikutnya), is true in the Future (or present) moment of time atau is Finally true. Operator F disebut dengan operator future atau operator “F”. G : benar pada semua state (saat ini dan semua state berikutnya), holds Globally in the moment of time. Operator G disebut dengan operator global atau operator “G”. U : benar hingga suatu state ketika benar, is true Until some future moment when is true. Operator U disebut dengan operator until atau operator “U”. W : akan selalu benar, kecuali bila benar maka boleh tidak benar Operator W disebut dengan operator “Weak-until” atau operaror “W”. R : akan selau benar hingga dan pada state ketika benar untuk kali pertama; bila tidak pernah benar, maka harus selamanya benar,

MZI (FIF Tel-U)

LTL

November 2015

13 / 74

Misalkan dan adalah dua formula LTL, berikut adalah makna intutif dari formula-formula dengan operator utama yang berupa operator temporal X : benar pada state berikutnya, is true in the neXt moment of time. Operator X disebut dengan operator next atau operator “X” F : benar pada suatu state (saat ini atau suatu state berikutnya), is true in the Future (or present) moment of time atau is Finally true. Operator F disebut dengan operator future atau operator “F”. G : benar pada semua state (saat ini dan semua state berikutnya), holds Globally in the moment of time. Operator G disebut dengan operator global atau operator “G”. U : benar hingga suatu state ketika benar, is true Until some future moment when is true. Operator U disebut dengan operator until atau operator “U”. W : akan selalu benar, kecuali bila benar maka boleh tidak benar Operator W disebut dengan operator “Weak-until” atau operaror “W”. R : akan selau benar hingga dan pada state ketika benar untuk kali pertama; bila tidak pernah benar, maka harus selamanya benar, the truth of Releases the truth of . Operator R disebut dengan operator release atau operator “R”. MZI (FIF Tel-U)

LTL

November 2015

13 / 74

Ilustrasi untuk Operator X, F, dan G.

MZI (FIF Tel-U)

LTL

November 2015

14 / 74

Notasi Lain

Beberapa literatur juga memakai notasi-notasi berikut: untuk menyatakan X untuk menyatakan F untuk menyatakan G U ( ; ) untuk menyatakan U W ( ; ) untuk menyatakan W R ( ; ) untuk menyatakan R

MZI (FIF Tel-U)

LTL

November 2015

15 / 74

Contoh Translasi Sederhana Berikut adalah beberapa contoh translasi sederhana yang melibatkan operator temporal pada LTL. 1

If a message is sent to a receiver, then the message will eventually be received atau dalam bahasa Indonesia: jika pesan dikirimkan ke suatu penerima, maka suatu saat pesan akan diterima. Misalkan proposisi yang digunakan adalah send_msg : pesan dikrimkan ke suatu penerima dan receive_msg : pesan diterima, maka translasinya menjadi:

MZI (FIF Tel-U)

LTL

November 2015

16 / 74


2

If a message is sent to a receiver, then the message will eventually be received atau dalam bahasa Indonesia: jika pesan dikirimkan ke suatu penerima, maka suatu saat pesan akan diterima. Misalkan proposisi yang digunakan adalah send_msg : pesan dikrimkan ke suatu penerima dan receive_msg : pesan diterima, maka translasinya menjadi: (send_msg) ! F (receive_msg). It is always the case that, if either ‘have_passport’or ‘have_ticket’is false, then in the next moment in time ‘board_f ligt’will also be false ditranslasikan menjadi:

MZI (FIF Tel-U)

LTL

November 2015

16 / 74


2

3

If a message is sent to a receiver, then the message will eventually be received atau dalam bahasa Indonesia: jika pesan dikirimkan ke suatu penerima, maka suatu saat pesan akan diterima. Misalkan proposisi yang digunakan adalah send_msg : pesan dikrimkan ke suatu penerima dan receive_msg : pesan diterima, maka translasinya menjadi: (send_msg) ! F (receive_msg). It is always the case that, if either ‘have_passport’or ‘have_ticket’is false, then in the next moment in time ‘board_f ligt’will also be false ditranslasikan menjadi: G ((:have_passport) _ (:have_ticket) ! X (:board_f light)). If something is born, then it is living up until the point in time that it becomes dead ditranslasikan menjadi:

MZI (FIF Tel-U)

LTL

November 2015

16 / 74


2

3

If a message is sent to a receiver, then the message will eventually be received atau dalam bahasa Indonesia: jika pesan dikirimkan ke suatu penerima, maka suatu saat pesan akan diterima. Misalkan proposisi yang digunakan adalah send_msg : pesan dikrimkan ke suatu penerima dan receive_msg : pesan diterima, maka translasinya menjadi: (send_msg) ! F (receive_msg). It is always the case that, if either ‘have_passport’or ‘have_ticket’is false, then in the next moment in time ‘board_f ligt’will also be false ditranslasikan menjadi: G ((:have_passport) _ (:have_ticket) ! X (:board_f light)). If something is born, then it is living up until the point in time that it becomes dead ditranslasikan menjadi: (born) ! (living) U (dead).

MZI (FIF Tel-U)

LTL

November 2015

16 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

17 / 74

Sintaks Formal LTL BNF untuk LTL Misalkan P = fp j p proposisi atomg menyatakan himpunan seluruh proposisi atom yang ditinjau dan p 2 P. Formula dide…nisikan dengan BNF berikut :

:= p j : j

^

j

_

j

!

jX jF jG j U j W j R Formula dengan operator logika proposisi lain seperti dan $ dapat dipandang sebagai ringkasan dari formula-formula dengan operator-operator yang terdapat pada BNF. Kita akan menulis > sebagai ringkasan dari _ : atau : _ . Kemudian kita juga akan menulis ? sebagai ringkasan dari ^ : atau : ^ .

Catatan Penulisan > dan ? biasanya hanya digunakan ketika kita meninjau formula logika predikat secara sintaks saja. Jika kita meninjau formula logika predikat secara sematik, maka kita akan menggunakan notasi T dan F, B dan S, atau 0 dan 1.

MZI (FIF Tel-U)

LTL

November 2015

18 / 74

Formula yang Terbentuk dengan Baik (Well-Formed Formula, WFF) De…nisi (Formula yang terbentuk dengan baik (well-formed formula, WFF)) Suatu formula LTL dikatakan sebagai formula yang terbentuk dengan baik (well-formed formula) bila dapat dikonstruksi dengan berhingga langkah (…nite step) berdasarkan BNF untuk LTL yang telah dijelaskan sebelumnya.

Catatan Untuk selanjutnya, istilah formula akan selalu berarti well-formed formula, kecuali bila disebutkan selain itu. Sebagai contoh, Up dan pGq bukan formula LTL karena

MZI (FIF Tel-U)

LTL

November 2015

19 / 74

Formula yang Terbentuk dengan Baik (Well-Formed Formula, WFF) De…nisi (Formula yang terbentuk dengan baik (well-formed formula, WFF)) Suatu formula LTL dikatakan sebagai formula yang terbentuk dengan baik (well-formed formula) bila dapat dikonstruksi dengan berhingga langkah (…nite step) berdasarkan BNF untuk LTL yang telah dijelaskan sebelumnya.

Catatan Untuk selanjutnya, istilah formula akan selalu berarti well-formed formula, kecuali bila disebutkan selain itu. Sebagai contoh, Up dan pGq bukan formula LTL karena U adalah operator biner dan G adalah operator uner.

MZI (FIF Tel-U)

LTL

November 2015

19 / 74

Presedens (Hirarki) Operator Logika pada LTL

Tabel urutan pengerjaan (presendens) operator logika pada LTL adalah Urutan 1 2 3

Urutan operator berdasarkan prioritas dari kiri ke kanan :; X; F; G U; R; W ^; _; ; !; $

Kita dapat menggunakan tanda kurung “(” dan “)” untuk memperjelas operasi yang harus didahulukan. Suatu formula dikatakan dalam fully parenthesized expression (FPE) bila urutan pengerjaan operator dan operand dalam formula tersebut sudah diperjelas dengan pemberian tanda kurung.

MZI (FIF Tel-U)

LTL

November 2015

20 / 74

Latihan Jika p; q; r; s adalah proposisi-proposisi atom, tentukan FPE dari formula-formula berikut: 1 2 3 4

Fp ^ Gq ! pWr

F (p ! Gr) _ :qUp FpW (qWr)

GFp ! F (Xq _ s)

Kita memiliki: (1)

MZI (FIF Tel-U)

LTL

November 2015

21 / 74


Fp ^ Gq ! pWr


GFp ! F (Xq _ s)

Kita memiliki: (1) ((Fp) ^ (Gq)) ! (pWr),

MZI (FIF Tel-U)

LTL

November 2015

21 / 74


Fp ^ Gq ! pWr


GFp ! F (Xq _ s)

Kita memiliki: (1) ((Fp) ^ (Gq)) ! (pWr), (2) F (p ! Gr) _ ((:q) Up),

MZI (FIF Tel-U)

LTL

November 2015

21 / 74


Fp ^ Gq ! pWr


GFp ! F (Xq _ s)

Kita memiliki: (1) ((Fp) ^ (Gq)) ! (pWr), (2) F (p ! Gr) _ ((:q) Up), (3) (Fp) W (qWr),

MZI (FIF Tel-U)

LTL

November 2015

21 / 74


Fp ^ Gq ! pWr


GFp ! F (Xq _ s)

Kita memiliki: (1) ((Fp) ^ (Gq)) ! (pWr), (2) F (p ! Gr) _ ((:q) Up), (3) (Fp) W (qWr), (4) G (Fp) ! F (X (q) _ s)

MZI (FIF Tel-U)

LTL

November 2015

21 / 74

Subformula LTL

Subformula LTL 1

Sebuah formula

2

adalah subformula dari

itu sendiri.

Jika dan adalah dua formula logika predikat yang dipakai untuk membangun formula yang lebih kompleks, maka dan dikatakan subformula sejati (atau subformula murni) dari .

3

Subformula bersifat transitif: jika , maka subformula dari .

subformula dari

dan

subformula dari

Contoh Misalkan

adalah formula pW (qUr), maka subformula dari

MZI (FIF Tel-U)

LTL

adalah (1)

November 2015

22 / 74

Subformula LTL

Subformula LTL 1

Sebuah formula

2


itu sendiri.


3


subformula dari

dan

subformula dari

Contoh Misalkan adalah formula pW (qUr), maka subformula dari pW (qUr), (2)

MZI (FIF Tel-U)

LTL

adalah (1)

November 2015

22 / 74

Subformula LTL

Subformula LTL 1

Sebuah formula

2


itu sendiri.


3


subformula dari

dan

subformula dari

Contoh Misalkan adalah formula pW (qUr), maka subformula dari pW (qUr), (2) qUr, (3)

MZI (FIF Tel-U)

LTL

adalah (1)

November 2015

22 / 74

Subformula LTL

Subformula LTL 1

Sebuah formula

2


itu sendiri.


3


subformula dari

dan

subformula dari

Contoh Misalkan adalah formula pW (qUr), maka subformula dari pW (qUr), (2) qUr, (3) p, (4)

MZI (FIF Tel-U)

LTL

adalah (1)

November 2015

22 / 74

Subformula LTL

Subformula LTL 1

Sebuah formula

2


itu sendiri.


3


subformula dari

dan

subformula dari

Contoh Misalkan adalah formula pW (qUr), maka subformula dari pW (qUr), (2) qUr, (3) p, (4) q, dan (5)

MZI (FIF Tel-U)

LTL

adalah (1)

November 2015

22 / 74

Subformula LTL

Subformula LTL 1

Sebuah formula

2


itu sendiri.


3


subformula dari

dan

subformula dari

Contoh Misalkan adalah formula pW (qUr), maka subformula dari pW (qUr), (2) qUr, (3) p, (4) q, dan (5) r.

MZI (FIF Tel-U)

LTL

adalah (1)

November 2015

22 / 74

Pohon Urai (Parse Tree) untuk Formula LTL Pohon urai (parse tree) dapat digunakan untuk menggambarkan struktur suatu formula LTL. Sebagai contoh, pohon urai untuk formula F (p ! Gr) _ :qUr adalah

MZI (FIF Tel-U)

LTL

November 2015

23 / 74

Pohon Urai (Parse Tree) untuk Formula LTL Pohon urai (parse tree) dapat digunakan untuk menggambarkan struktur suatu formula LTL. Sebagai contoh, pohon urai untuk formula F (p ! Gr) _ :qUr adalah

MZI (FIF Tel-U)

LTL

November 2015

23 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

24 / 74

Model (Sistem Transisi) untuk LTL Semantik formula LTL ditinjau pada sebuah model yang juga disebut sebagai sistem transisi/ transition system (beberapa literatur juga menyebutnya dengan struktur Kripke/ Kripke structure).

De…nisi (Model/ Sistem Transisi untuk LTL) Sebuah model atau sistem transisi untuk LTL dengan himpunan proposisi atom P adalah tripel M = (S; !; L) dengan: 1

S adalah himpunan state

2

! adalah relasi biner pada S, dengan perkataan lain ! S S yang memenuhi sifat: untuk setiap s 2 S terdapat s0 2 S sehingga (s; s0 ) 2!, hal ini juga dapat ditulis: untuk setiap s 2 S terdapat s0 2 S sehingga s ! s0 (dalam matematika diskret kita mengenal istilah bahwa ! adalah relasi total pada S)

3

L adalah fungsi pelabelan dari himpunan seluruh state (yaitu S) ke himpunan kuasa proposisi atom (yaitu 2P ), L dapat ditulis sebagai L : S ! 2P . MZI (FIF Tel-U)

LTL

November 2015

25 / 74

Contoh Model Sederhana Misalkan M = (S; !; L) adalah tripel yang ditinjau atas himpunan propososi atom P = fp; q; rg dengan S = fs0 ; s1 ; s2 g

!= f(s0 ; s1 ) ; (s0 ; s2 ) ; (s1 ; s0 ) ; (s1 ; s2 ) ; (s2 ; s2 )g, hal ini juga dapat ditulis dengan s0 ! s1 , s0 ! s2 , s1 ! s0 , s1 ! s2 , s2 ! s2 L : S ! 2P dengan L (s0 ) = fp; qg, L (s1 ) = fq; rg, L (s2 ) = r, hal ini juga dapat dinyatakan dalam tabel berikut: si L (si )

s0 fp; qg

s1 fq; rg

s2 r

Label ini berarti proposisi p dan q benar di s0 , proposisi q dan r benar di s1 , dan proposisi r benar di s2 . Kemudian karena r 62 L (s0 ) maka r salah di s0 , karena p 62 L (s1 ) maka p salah di s1 , dan karena p; q 62 L (s2 ) maka p maupun q salah di s2 .

MZI (FIF Tel-U)

LTL

November 2015

26 / 74

Tripel M adalah model LTL yang dapat digambarkan dalam graf berarah dengan label-label berikut

Relasi transisi ! pada M harus bersifat total, apabila self loop pada s2 dihilangkan, maka M tidak lagi menjadi model LTL. Jika kita menemukan suatu tripel M yang relasi transisinya tidak bersifat total, maka kita dapat mengkonstruksi model M0 dengan cara: 1

2

untuk setiap s 2 S dengan yang tidak memiliki s0 2 S sehingga s ! s0 , tambahkan state sd yang memenuhi s ! sd

pada state sd kita dapat menambahkan self loop sehingga berlaku sd ! sd

Notasi sd merepresentasikan state deadlock. MZI (FIF Tel-U)

LTL

November 2015

27 / 74

Contoh Penambahan State Deadlock

MZI (FIF Tel-U)

LTL

November 2015

28 / 74

MZI (FIF Tel-U)

LTL

November 2015

29 / 74

Lintasan (Path) pada Model De…nisi (Lintasan (path) pada model LTL) Sebuath lintasan (path) pada model M = (S; !; L) adalah barisan tak berhingga state 1 ; 2 ; 3 ; : : : dengan sifat: 1

i

2

i

2 S untuk setiap i !

i+1

1

untuk setiap i

1

Selanjutnya lintasan (path) pada model tersebut akan dinotasikan dengan . Suatu lintasan akan dinotasikan dengan . 1 ! 2 ! 3 ! Tinjau kembali model LTL berikut

MZI (FIF Tel-U)

LTL

November 2015

30 / 74

Salah satu lintasan pada model tersebut adalah = =

1

!

!

2

3

i

De…nisi (Su…ks i untuk lintasan, Misalkan = dan i 2maka

1 i

!

s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 !

)

! 2! 3! adalah sebuah lintasan pada model LTL M adalah lintasan yang dimulai dari state i , yaitu i

=

i

!

i+1

!

i+1

!

,

sehingga kita memiliki

MZI (FIF Tel-U)

1

=

2

=

1

!

2

!

3

LTL

!

= ,

November 2015

31 / 74


1

!

!

2

3

i


1 i

!

s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 !

)


=

i

!

i+1

!

i+1

!

,

sehingga kita memiliki 1

MZI (FIF Tel-U)

=

1

2

=

2

3

=

!

!

2 3

!

!

3 4

LTL

!

!

= , ,

November 2015

31 / 74


1

!

!

2

3

i


1 i

!

s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 !

)


=

i

!

i+1

!

i+1

!

,

sehingga kita memiliki 1

MZI (FIF Tel-U)

=

1

2

=

2

3

=

3

!

! !

2 3 4

!

! !

3 4 5

LTL

!

! !

= , , , dan seterusnya

November 2015

31 / 74

Contoh Bila

= s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 ! 2

, maka kita memiliki

=

MZI (FIF Tel-U)

LTL

November 2015

32 / 74

Contoh Bila

= s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 ! 2 4

= =

MZI (FIF Tel-U)


s0 ! s1 ! s0 ! s2 ! s2 ! s2 !

LTL

November 2015

32 / 74

Contoh Bila

= s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 ! 2 4 5

= = =

MZI (FIF Tel-U)


s0 ! s1 ! s0 ! s2 ! s2 ! s2 ! s0 ! s2 ! s2 ! s2 !

LTL

November 2015

32 / 74

Contoh Bila

= s1 ! s0 ! s1 ! s0 ! s2 ! s2 ! s2 ! 2 4 5

= = =

MZI (FIF Tel-U)


s0 ! s1 ! s0 ! s2 ! s2 ! s2 ! s0 ! s2 ! s2 ! s2 ! s2 ! s2 ! s2 !

=

LTL

6

=

=

n

untuk n

5

November 2015

32 / 74

Pada model LTL sebelumnya, semua lintasan pada M dapat direpresentasikan dalam pohon (tree) berikut

MZI (FIF Tel-U)

LTL

November 2015

33 / 74

Semantik LTL pada Sebuah Lintasan De…nisi ( j= )

Misalkan M = (S; !; L) adalah sebuah model LTL dan = 1! 2! 3! adalah sebuah lintasan pada M. Untuk setiap formula LTL , notasi j= berarti lintasan memenuhi formula . Relasi j= dide…nisikan sebagai berikut De…nisi terkait operator logika proposisi: j= > (ini berarti > selalu benar/ dipenuhi pada sembarang lintasan apapun). 6j= ? (ini berarti ? selalu salah/ tak dipenuhi pada sembarang lintasan apapun). j= p jikka p 2 L ( j= : jikka j= j= j=

1 1 1

^ _

6j=

2

jikka

2

jikka

!

MZI (FIF Tel-U)

2

1 ).

(ini berarti j= j=

1

dan

1

atau

jikka apabila

j=

tidak dipenuhi pada lintasan ). j=

2.

1

maka

j=

LTL

2.

j=

2.

November 2015

34 / 74

De…nisi tekait operator temporal: j= X jikka

2

j=

j= F jikka terdapat i

j= G jikka untuk semua i

j= U jikka terdapat i memenuhi j j= j= W I

I

I

i

1 berlaku 1 sehingga

i

j=

j=

j= dan setiap 1

j

i

1

jikka:

terdapat i 1 sehingga i j= dan setiap 1 atau untuk setiap i 1 berlaku i j=

j= R I

i

1 yang memenuhi

1 memenuhi

j

i

j

i memenuhi

j

j= ,

jikka:

terdapat i 1 sehingga i j= dan setiap 1 untuk setiap i 1 berlaku i j=

MZI (FIF Tel-U)

LTL

j

j= , atau

November 2015

35 / 74

De…nisi Operator Temporal dengan Logika Predikat

Misalkan domain untuk i dan j adalah N = f1; 2; 3; : : :g. j= X jikka

2

j= F jikka 9i

j= .

j= G jikka 8i j= U j= W j= R

jikka 9i jikka 9i jikka 9i

MZI (FIF Tel-U)

i

i

j=

j=

. .

^8j (1 ^8j (1 ^8j (1

i

j

j= i 1) !

i

j i

j

j= i 1) !

j= i) !

LTL

j

j=

j

j

j=

. i

_ 8i

j= _ 8i

i

j=

j=

.

.

November 2015

36 / 74

Ilustrasi Intuitif

MZI (FIF Tel-U)

LTL

November 2015

37 / 74

Makna Operator U dan W Perhatikan bahwa baik operator U maupun operator W tidak menjelaskan apa yang harus terjadi setelah “until” tercapai. Hal ini dapat berbeda dengan “until” yang terdapat pada bahasa alami.

Contoh Perhatikan kalimat berikut: “John smoked until he was 22 years old” berarti bahwa: “John continually smoked up until he was 22 years old” “John gave up smoking after his 22nd birthday ” Jika s adalah proposisi “John smoke” dan t adalah proposisi “John is 22 years old” maka translasi yang tepat dari “John smoked until he was 22 years old” adalah:

MZI (FIF Tel-U)

LTL

November 2015

38 / 74

Makna Operator U dan W Perhatikan bahwa baik operator U maupun operator W tidak menjelaskan apa yang harus terjadi setelah “until” tercapai. Hal ini dapat berbeda dengan “until” yang terdapat pada bahasa alami.

Contoh Perhatikan kalimat berikut: “John smoked until he was 22 years old” berarti bahwa: “John continually smoked up until he was 22 years old” “John gave up smoking after his 22nd birthday ” Jika s adalah proposisi “John smoke” dan t adalah proposisi “John is 22 years old” maka translasi yang tepat dari “John smoked until he was 22 years old” adalah: sU (t ^ G:s), bukan sUt karena formula sUt juga dapat benar ketika “John smoked until he was 22 years old, yet he stopped before he died in 80.”

MZI (FIF Tel-U)

LTL

November 2015

38 / 74

Semantik LTL pada Sebuah Model

De…nisi Misalkan M = (S; !; L) adalah model LTL, s 2 S, dan adalah sebuah formula LTL. Kita katakan terpenuhi (satis…able) pada state s, ditulis M; s j= , apabila untuk setiap lintasan

MZI (FIF Tel-U)

pada M yang dimulai di s memenuhi

LTL

j= .

November 2015

39 / 74

Latihan Dari model LTL berikut:

Periksa apakah: 1 2 3 4 5

M; s0 j= p ^ q M; s0 j= :r M; s0 j= >

M; s0 j= Xr

M; s0 j= X (q ^ r)

MZI (FIF Tel-U)

LTL

November 2015

40 / 74

1

M; s0 j= p ^ q karena untuk setiap lintasan = s0 ! kita memiliki p; q 2 L (s0 ), akibatnya j= p ^ q, sehingga M; s0 j= p ^ q.

MZI (FIF Tel-U)

LTL

November 2015

41 / 74

1

2


M; s0 j= :r karena untuk setiap lintasan = s0 ! kita memiliki r 62 L (s0 ), akibatnya 6j= r, sehingga j= :r, sehingga M; s0 j= :r.

MZI (FIF Tel-U)

LTL

November 2015

41 / 74

1

2

3


M; s0 j= :r karena untuk setiap lintasan = s0 ! kita memiliki r 62 L (s0 ), akibatnya 6j= r, sehingga j= :r, sehingga M; s0 j= :r. M; s0 j= >, karena berdasarkan de…nisi setiap lintasan akibatnya M; s0 j= >.

MZI (FIF Tel-U)

LTL

memenuhi

j= >,

November 2015

41 / 74

1

2

3

4



memenuhi

M; s0 j= Xr, karena lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! , hanya memiliki dua kemungkinan untuk I

I

= s0 ! s1 ! = s0 ! s2 !

, karena r 2 L (s1 ), maka , karena r 2 L (s2 ), maka

2

2

j= r, akibatnya j= r, akibatnya

Karena setiap lintasan yang dimulai dari s0 memenuhi M; s0 j= Xr.

MZI (FIF Tel-U)

LTL

j= >,

1,

yaitu:

j= Xr, j= Xr.

j= Xr, maka berlaku

November 2015

41 / 74

1

2

3

4



M; s0 j= Xr, karena lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! , hanya memiliki dua kemungkinan untuk I

I

5

memenuhi

= s0 ! s1 ! = s0 ! s2 !

, karena r 2 L (s1 ), maka , karena r 2 L (s2 ), maka

2

2

j= r, akibatnya j= r, akibatnya

Karena setiap lintasan yang dimulai dari s0 memenuhi M; s0 j= Xr.

j= >,

1,

yaitu:

j= Xr, j= Xr.

j= Xr, maka berlaku

M; s0 6j= X (q ^ r), atau dapat ditulis M; s0 j= :X (q ^ r). Tinjau lintasan = s0 ! s2 ! s2 ! , kita memiliki q 62 L (s2 ), akibatnya 2 j= :q, sehingga j= X:q. Akibatnya tidak mungkin M; s0 j= X (q ^ r). Jadi haruslah M; s0 6j= X (q ^ r).

MZI (FIF Tel-U)

LTL

November 2015

41 / 74

Latihan Dari model LTL berikut:

Periksa apakah: 1 2 3 4 5

M; s0 j= G: (p ^ r) M; s0 j= GFr

M; s0 j= GFp ! GFr

M; s0 j= GFr ! GFp M; s0 j= pUr

MZI (FIF Tel-U)

LTL

November 2015

42 / 74

1

M; s0 j= G: (p ^ r) karena setiap lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! , hanya memiliki kemungkinan bahwa 2 fs ; s ; s g dan tidak ada state pada fs0 ; s1 ; s2 g dengan sifat p dan r i 0 1 2 keduanya benar pada state tersebut.

MZI (FIF Tel-U)

LTL

November 2015

43 / 74

1

2

M; s0 j= G: (p ^ r) karena setiap lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! , hanya memiliki kemungkinan bahwa 2 fs ; s ; s g dan tidak ada state pada fs0 ; s1 ; s2 g dengan sifat p dan r i 0 1 2 keduanya benar pada state tersebut. M; s0 j= GFr, karena untuk setiap lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! kita memiliki j= GFr. Hal ini dapat dijelaskan sebagai berikut. Kita dapat mengklasi…kasikan menjadi dua kategori: I

I

memuat s2 , akibatnya akan berlaku j= GFr karena jika memuat s2 pastilah berbentuk = ! s2 ! s2 ! s2 ! dan r 2 L (s2 ) tidak memuat s2 , akibatnya akan berlaku j= GFr karena pasti berbetuk: = ! s0 ! s1 ! s0 ! s1 ! dan r 2 L (s1 ).

MZI (FIF Tel-U)

LTL

November 2015

43 / 74

1

2


I

3


M; s0 j= GFp ! GFr, karena untuk setiap lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! kita memiliki j= GFp ! GFr. Hal ini dapat dijelaskan sebagai berikut. Kita dapat mengklasi…kasikan menjadi dua kategori: I I

memuat s2 , akibatnya akan berlaku j= GFr, jadi j= GFp ! GFr tidak memuat s2 , akibatnya akan berlaku j= GFr, jadi j= GFp ! GFr.

MZI (FIF Tel-U)

LTL

November 2015

43 / 74

1

2


I

3

M; s0 j= GFp ! GFr, karena untuk setiap lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! kita memiliki j= GFp ! GFr. Hal ini dapat dijelaskan sebagai berikut. Kita dapat mengklasi…kasikan menjadi dua kategori: I I

4


memuat s2 , akibatnya akan berlaku j= GFr, jadi j= GFp ! GFr tidak memuat s2 , akibatnya akan berlaku j= GFr, jadi j= GFp ! GFr.

M; s0 6j= GFr ! GFp atau dapat ditulis M; s0 j= : (GFr ! GFp). Tinjau lintasan = s0 ! s2 ! s2 ! , kita memiliki j= GFr tetapi j= :GFp karena p 62 L (s2 ). MZI (FIF Tel-U)

LTL

November 2015

43 / 74

5

M; s0 j= pUr, karena untuk setiap lintasan yang dimulai dari s0 , yaitu = s0 ! 1 ! 2 ! kita memiliki j= pUr. Hal ini dapat dijelaskan sebagai berikut. Kita dapat mengklasi…kasikan menjadi dua kategori: 1

F F

= s0 ! s1 ! = s0 ! s2 !

MZI (FIF Tel-U)

, karena p 2 L (s0 ) dan r 2 L (s1 ), maka berlaku , karena p 2 L (s0 ) dan r 2 L (s1 ), maka berlaku

LTL

j= pUr, j= pUr.

November 2015

44 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

45 / 74


Dalam computer science dan software engineering, logika temporal digunakan untuk membuat formalisasi dari sistem reaktif-konkuren (concurrent reactive systems), salah satu contohnya adalah lampu lalu lintas (tra¢ c light). Untuk mendesain sistem-sistem tersebut secara formal, perlu ditinjau beberapa sifat yang harus dipenuhi oleh sistem tersebut, yaitu: 1

Sifat keamanan (safety properties).

2

Sifat ketercapaian (liveness properties).

3

Karakterisasi “selalu terjadi secara berkala” (in…nitely often).

4

Sifat keadilan (fairness properties).

MZI (FIF Tel-U)

LTL

November 2015

46 / 74

Sifat Keamanan (Safety Properties) Sifat keamanan (safety properties) berarti: sesuatu hal yang buruk tidak boleh pernah terjadi (something bad will not happen). Misalkan merepresentasikan suatu hal buruk, maka safety properties biasanya dituliskan dalam formula LTL sebagai G: .

Contoh Pada lampu lalu lintas, lampu merah, kuning, dan hijau tidak boleh menyala bersamaan: G: (red ^ yellow ^ green). Pada suatu reaktor nuklir, suhu reaktor tidak boleh lebih dari 1000 C : G: (reactor_temp: > 1000). Pada suatu sistem tidak boleh ada pembagian dengan 0 : G: ((x = 0) ^ X (y = a=0)).

MZI (FIF Tel-U)

LTL

November 2015

47 / 74

Sifat Ketercapaian (Liveness Properties) Sifat keamanan (safety properties) berarti: sesuatu hal yang baik harus dapat terjadi (something good will happen). Misalkan merepresentasikan suatu hal baik, maka liveness properties biasanya dituliskan dalam formula LTL sebagai F .

Contoh Pada lampu lalu lintas, jika lampu merah menyala maka suatu saat lampu hijau akan menyala: G (red ! Fgreen). Pada suatu sistem, jika proses dijalankan maka suatu saat proses akan berhenti: G (start ! Fterminate). Pada suatu sistem, jika pesan dikirimkan, maka pesan sautu saat pesan akan diterima: G (send ! Freceived).

MZI (FIF Tel-U)

LTL

November 2015

48 / 74

Selalu Terjadi Secara Berkala (In…nitely Often)

Misalkan adalah sebuah formula LTL, kombinasi dari operator G dan F sebagai GF dapat ditranslasikan sebagai: “ selalu terjadi secara berkala”. Perhatikan bahwa 1

M; s j= GF berarti setiap lintasan j= GF .

MZI (FIF Tel-U)

LTL

yang dimulai dari

memenuhi

November 2015

49 / 74



2

M; s j= GF berarti setiap lintasan yang dimulai dari j= GF . j= GF berarti untuk setiap i 1 berlaku i j= F .

MZI (FIF Tel-U)

LTL

memenuhi

November 2015

49 / 74



2 3

M; s j= GF berarti setiap lintasan yang dimulai dari j= GF . j= GF berarti untuk setiap i 1 berlaku i j= F . i

j= F berarti terdapat j

MZI (FIF Tel-U)

i sehingga

LTL

j

memenuhi

j= .

November 2015

49 / 74



2 3 4



Akibatnya j j= .

MZI (FIF Tel-U)

i sehingga

j

j= GF berarti untuk setiap i

LTL

j= .

1 terdapat j

memenuhi

i sehingga

November 2015

49 / 74



2 3 4

5



Akibatnya j j= .

i sehingga

j

j= GF berarti untuk setiap i

j= .

1 terdapat j

memenuhi

i sehingga

Ini berarti akan terjadi secara terus menerus (“secara berkala, namun tidak harus regular”) atau terjadi in…nitely often.

MZI (FIF Tel-U)

LTL

November 2015

49 / 74

Contoh Pada lampu lalu lintas, lampu kuning menyala secara berkala: GFyellow. Pada perlintasan kereta api, portal ditutup secara berkala: GF (gate = closed).

Catatan Formula GF tidak mengimplikasikan G , tetapi G mengimplikasikan GF .

MZI (FIF Tel-U)

LTL

November 2015

50 / 74

Sifat Keadilan (Fairness) Ada beberapa jenis sifat keadilan (fairness properties) dalam pemodelan sistem reaktif. Misalkan attempt dan succeed adalah dua proposisi yang ditinjau. 1

GFattempt ! GFsucceed : if we attempt something in…nitely often, then we will succeed in…nitely often (disebut juga sebagai keadilan kuat/ strong fairness)

2

GFattempt ! Fsucceed : if we attempt something in…nitely often, then we will succeed at least one

3

Gattempt ! GFsucceed : if we attempt something continuosly, then we will succeed in…nitely often

4

Gattempt ! Fsucceed : if we attempt something continuosly, then we will succeed at least one

Contoh Pada lampu lalu lintas, jika ada daya listrik, maka lampu kuning akan menyala secara berkala: Gpower ! GFyellow MZI (FIF Tel-U)

LTL

November 2015

51 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

52 / 74

Sifat-sifat Formula Berdasarkan Semantiknya De…nisi Misalkan 1

2

3

4

5

adalah sebuah formula LTL:

formula dikatakan absah (valid) atau tautologi apabila M; s j= sembarang status s pada sembarang model M. formula dikatakan terpenuhi (satis…able) apabila M; s j= status s pada suatu model M.

untuk suatu

formula dikatakan kontradiksi (contradictory ) apabila M; s 6j= sembarang status s pada sembarang model M. formula dikatakan tersalahkan (falsi…able) apabila M; s 6j= status s pada suatu model M.

untuk

untuk

untuk suatu

formula dikatakan kontingensi (contingency ) apabila bukan formula yang bersifat absah dan bukan pula formula yang bersifat kontradiksi.

MZI (FIF Tel-U)

LTL

November 2015

53 / 74

Beberapa Teorema Penting

Teorema Misalkan

adalah sebuah formula LTL, maka berlaku:

1

formula

2

absah (valid) jika dan hanya jika : kontradiksi,

formula terpenuhi (satis…able) jika dan hanya jika : tersalahkan (falsi…able),

3

formula valid),

terpenuhi (satis…able) jika dan hanya jika : tidak absah (tidak

4

formula

absah (valid) jika dan hanya jika : tidak terpenuhi.

MZI (FIF Tel-U)

LTL

November 2015

54 / 74

Konsekuensi Logis dan Kesetaraan Logika

De…nisi Misalkan dan Formula dan formula

adalah dua formula LTL: dikatakan setara atau ekuivalen (logically equivalent) jika $

merupakan tautologi. Hal ini dituliskan dengan atau , . Formula dikatakan sebagai konsekuensi logis (logical consequence) dari formula ! merupakan tautologi. Hal ini dituliskan dengan

MZI (FIF Tel-U)

LTL

jika

) .

November 2015

55 / 74

Beberapa Ekuivalensi Terkait Operator Temporal Teorema Misalkan 1 2 3

:G :F

:X

adalah formula LTL, maka berlaku: F: G: X:

Ini berarti operator F dan G saling dual dan X bersifat dual dengan dirinya sendiri.

Teorema Misalkan 1 2

dan

:( U ) :( R )

MZI (FIF Tel-U)

adalah dua formula LTL, maka berlaku: : R:

: U:

LTL

November 2015

56 / 74

Teorema Misalkan 1 2

dan

adalah dua formula LTL, maka berlaku:

F( _ )

F _F

G( ^ )

G ^G

Teorema Misalkan 1

F

2

G

adalah formula LTL, maka berlaku: >U

?R

Teorema Misalkan 1

U

2

W

3

W

4

R

dan

adalah dua formula LTL, maka berlaku:

W ^F

U _G

R( _ )

W( ^ )

MZI (FIF Tel-U)

LTL

November 2015

57 / 74

Beberapa Bukti Formal Ekuivalensi Terkait Operator Temporal Bukti (:G

F: )

Misalkan M adalah sembarang model dan lintasan pada M. 1

j= :G ,

MZI (FIF Tel-U)

=

1

!

2

!

sembarang

6j= G

LTL

November 2015

58 / 74


F: )

Misalkan M adalah sembarang model dan lintasan pada M. 1 2

j= :G ,

Kita memiliki

MZI (FIF Tel-U)

6j= G

=

j= G , untuk setiap i

LTL

1

!

2

sembarang

!

1 berlaku

i

j= .

November 2015

58 / 74


F: )


j= :G ,

2

Kita memiliki

3

Ini berarti

MZI (FIF Tel-U)

6j= G

=


6j= G , terdapat i

1

!

2

sembarang

!

1 berlaku

i

j= .

1 sehingga tidak berlaku

LTL

i

j= .

November 2015

58 / 74


F: )


j= :G ,

2

Kita memiliki

3

Ini berarti

4

Ini berarti

MZI (FIF Tel-U)

6j= G

=


6j= G , terdapat i 6j= G , terdapat i

1

!

2

sembarang

!

1 berlaku

i

j= .

1 sehingga tidak berlaku 1 sehingga berlaku

LTL

i

i

6j= .

j= .

November 2015

58 / 74


F: )


j= :G ,

2

Kita memiliki

3

Ini berarti

4

Ini berarti

5

Ini berarti

MZI (FIF Tel-U)

6j= G

=


1

!

2

sembarang

!

1 berlaku

i

j= .

6j= G , terdapat i

1 sehingga tidak berlaku

6j= G , terdapat i

1 sehingga

6j= G , terdapat i

1 sehingga berlaku

LTL

i

j= : .

i

i

6j= .

j= .

November 2015

58 / 74


F: )


j= :G ,

2

Kita memiliki

3

Ini berarti

4

Ini berarti

5

Ini berarti Ini berarti

6

MZI (FIF Tel-U)

6j= G

=



1

!

2

sembarang

!

1 berlaku

i

j= .


6j= G , terdapat i 1 sehingga 6j= G , berlaku j= F: .

LTL

i

j= : .

i

i

6j= .

j= .

November 2015

58 / 74


F: )


j= :G ,

2

Kita memiliki

3

Ini berarti

4

Ini berarti

5

Ini berarti Ini berarti

6 7

Ini berarti

6j= G



1

!

j= G , berlaku

2

sembarang

!

1 berlaku

i

j= .


6j= G , terdapat i 1 sehingga 6j= G , berlaku j= F: .

Bukti formal untuk :F MZI (FIF Tel-U)

=

i

j= : .

i

i

6j= .

j= .

j= F:

G: dapat diperoleh dengan cara serupa.

LTL

November 2015

58 / 74

Bukti (:X

X: )


j= :X ,

MZI (FIF Tel-U)

=

1

!

1

!

sembarang

6j= X .

LTL

November 2015

59 / 74

Bukti (:X

X: )


j= :X ,

Kita memiliki

MZI (FIF Tel-U)

6j= X .

j= X , berlaku

2

LTL

=

1

!

1

!

sembarang

j= .

November 2015

59 / 74

Bukti (:X

X: )

Misalkan M adalah sembarang model dan lintasan pada M. 1 2 3

j= :X ,

Kita memiliki Ini berarti

MZI (FIF Tel-U)

6j= X .

j= X , berlaku

6j= X , berlaku

2

2

=

1

!

1

!

sembarang

j= .

6j= .

LTL

November 2015

59 / 74

Bukti (:X

X: )


j= :X ,

Kita memiliki

3

Ini berarti

4

Ini berarti

MZI (FIF Tel-U)

6j= X .

j= X , berlaku

6j= X , berlaku 6j= X , berlaku

2 2

2

=

1

!

1

!

sembarang

j= .

6j= .

j= : .

LTL

November 2015

59 / 74

Bukti (:X

X: )


j= :X ,

Kita memiliki

3

Ini berarti

4

Ini berarti

5

Ini berarti

MZI (FIF Tel-U)

6j= X .

j= X , berlaku

6j= X , berlaku

2

6j= X , berlaku

2

6j= X , berlaku

2

2

=

1

!

1

!

sembarang

j= .

6j= .

j= : .

j= X: .

LTL

November 2015

59 / 74

Bukti (:X

X: )


j= :X ,

Kita memiliki

3

Ini berarti

4

Ini berarti

5

Ini berarti

6

Ini berarti

MZI (FIF Tel-U)

6j= X .

j= X , berlaku

6j= X , berlaku

2

6j= X , berlaku

2

6j= X , berlaku j= :X , berlaku

2

2

=

1

!

1

!

sembarang

j= .

6j= .

j= : .

j= X: .

j= X: .

LTL

November 2015

59 / 74

Bukti (: ( U )

: R: )


j= : ( U ) ,

MZI (FIF Tel-U)

=

1

!

2

!

sembarang

6j= U .

LTL

November 2015

60 / 74

Bukti (: ( U )

: R: )


j= : ( U ) ,

Kita memiliki 9i

^8j (1

MZI (FIF Tel-U)

=

1

!

2

!

sembarang

6j= U .

j= U , berlaku i j= j i 1) ! j j=

LTL

.

November 2015

60 / 74

Bukti (: ( U )

: R: )


j= : ( U ) ,

Kita memiliki 9i

3

^8j (1

Ini berarti

MZI (FIF Tel-U)

1

!

2

!

sembarang

6j= U .


6j= U

=

, berlaku 8i

. i

_9j (1

LTL

j

i

6j=

1) ^

j

6j=

November 2015

.

60 / 74

Bukti (: ( U )

: R: )


j= : ( U ) ,

Kita memiliki 9i

^8j (1

1

!

2

!

sembarang

6j= U .


3

Ini berarti

6j= U

, berlaku 8i

4

Ini berarti

6j= U

, berlaku 8i

MZI (FIF Tel-U)

=

LTL

. i

_9j (1

j

_9j (1

j

i i

i

6j=

1) ^

j= : 1) ^

j

6j=

j

j= :

November 2015

. .

60 / 74

Bukti (: ( U )

: R: )


j= : ( U ) ,

Kita memiliki 9i

^8j (1

1

!

2

!

sembarang

6j= U .


3

Ini berarti

6j= U

, berlaku 8i

4

Ini berarti

6j= U

, berlaku 8i

5

Ini berarti

6j= U

, berlaku 8i

MZI (FIF Tel-U)

=

LTL

. i

_9j (1

j

_9j (1

j

_9j (1

j

i i

i i

i

6j=

1) ^

j= : 1) ^ 6j= : 1) ^

j

6j=

j

j= :

j

j= :

November 2015

. . .

60 / 74

1

Ini berarti 8i

6j= U

! 9j (1

MZI (FIF Tel-U)

j

, berlaku i j= i 1) ^

j

j= :

LTL

.

November 2015

61 / 74

1

Ini berarti 8i

2

6j= U

! 9j (1

j


Formula logika predikat 8i benar bila:

MZI (FIF Tel-U)

j

.

j= :

! 9j (1

LTL

i

j

i

j=

1) ^

j

j= :

bernilai

November 2015

61 / 74

1

Ini berarti 8i

2

6j= U

! 9j (1

j


Formula logika predikat 8i benar bila: I

i

j

! 9j (1

j= selalu salah, ini artinya kondisi 8i i j= :

MZI (FIF Tel-U)

.

j= :

i

j= :

LTL

i

j

i

j=

1) ^

j

j= :

bernilai

untuk setiap i, sehingga diperoleh

November 2015

61 / 74

1

Ini berarti 8i

2

6j= U

! 9j (1

j



I

j

.

j= :

! 9j (1

i

j

i

j=

1) ^

j

j= :

bernilai

i

j= selalu salah, ini artinya i j= : untuk setiap i, sehingga diperoleh kondisi 8i i j= : i j= dapat benar untuk suatu i, jika kondisi ini terjadi maka haruslah terdapat j i 1 sehingga j j= : . Pada kondisi ini kita juga harus memiliki j j= : dan secara umum k j= : bila 1 k i 1 (argumen detail diserahkan kepada pembaca sebagai latihan). Akibatnya diperoleh j 9j j= : ^ 8k ((1 k j) ! j= : ) .

MZI (FIF Tel-U)

LTL

November 2015

61 / 74

1

Ini berarti 8i

2

! 9j (1

j



I

3

6j= U

j

.

j= :

! 9j (1

i

j

i

j=

1) ^

j

j= :

bernilai

i


Kondisi di atas dapat ditulis ulang sebagai: i j= : 9i _ 8i ^8j ((1 j i) ! j= : ) j= : R: .

MZI (FIF Tel-U)

LTL

i

j= :

, yang setara dengan

November 2015

61 / 74

1

Ini berarti 8i

2

6j= U

! 9j (1

j


I

3

4


j

.

j= :

! 9j (1

i

j

i

j=

1) ^

j

j= :

bernilai

i


Kondisi di atas dapat ditulis ulang sebagai: i j= : 9i _ 8i ^8j ((1 j i) ! j= : ) j= : R: . Jadi i 6j= U j= : R: . MZI (FIF Tel-U)

,

j= : R:

atau

LTL

i

j= :

, yang setara dengan

j= : ( U ) setara dengan dengan November 2015

61 / 74

Bukti (F ( _ )

F _F )

Misalkan M adalah sembarang model dan lintasan pada M. j= F ( _ )

MZI (FIF Tel-U)

=

1

!

2

!

sembarang

,

LTL

November 2015

62 / 74

Bukti (F ( _ )

F _F )


,

=

1

!

2

!

sembarang

i 9i j= _ i j= (de…nisi operator F)

,

MZI (FIF Tel-U)

LTL

November 2015

62 / 74

Bukti (F ( _ )

F _F )


, , ,

MZI (FIF Tel-U)

=

1

!

2

i 9i j= _ i j= (de…nisi operator F) 9i i j= _ 9i i j= (ekuivalensi 9x ( _ )

LTL

!

sembarang

9x _ 9x )

November 2015

62 / 74

Bukti (F ( _ )

F _F )


, , ,

=

1

!

2

i 9i j= _ i j= (de…nisi operator F) 9i i j= _ 9i i j= (ekuivalensi 9x ( _ ) j= F _ F . (de…nisi operator F)

!

sembarang

9x _ 9x )

Bukti formal untuk G ( ^ ) dapat diperoleh dengan cara serupa.

MZI (FIF Tel-U)

LTL

November 2015

62 / 74

Adequate Set of Connectives pada LTL Pada logika proposisi, kita telah melihat bahwa himpunan f:; ^g, f:; _g, f:; !g, f"g, dan f#g adalah adequate set of connectives. Ini berarti semua operator logika lain pada logika proposisi dapat dinyatakan hanya dengan operator-operator yang terdapat pada adequate set of connectives tersebut. Dengan meninjau ekuivalensi semantik pada LTL, kita memiliki sifat-sifat berikut:

MZI (FIF Tel-U)

LTL

November 2015

63 / 74

Adequate Set of Connectives pada LTL Pada logika proposisi, kita telah melihat bahwa himpunan f:; ^g, f:; _g, f:; !g, f"g, dan f#g adalah adequate set of connectives. Ini berarti semua operator logika lain pada logika proposisi dapat dinyatakan hanya dengan operator-operator yang terdapat pada adequate set of connectives tersebut. Dengan meninjau ekuivalensi semantik pada LTL, kita memiliki sifat-sifat berikut: 1

Operator temporal X tidak dapat dinyatakan dengan operator-operator temporal lain.

MZI (FIF Tel-U)

LTL

November 2015

63 / 74



2

Operator F dapat dinyatakan dengan operator U, kita memiliki F

MZI (FIF Tel-U)

LTL

November 2015

63 / 74



2

Operator F dapat dinyatakan dengan operator U, kita memiliki F >U . Karena operator G adalah dual dari operator F, maka operator G juga dapat dinyatakan dengan operator U. Kita memiliki G

MZI (FIF Tel-U)

LTL

November 2015

63 / 74



2

Operator F dapat dinyatakan dengan operator U, kita memiliki F >U . Karena operator G adalah dual dari operator F, maka operator G juga dapat dinyatakan dengan operator U. Kita memiliki G :F: : (>U: ).

MZI (FIF Tel-U)

LTL

November 2015

63 / 74



2


3

Berdasarkan de…nisi operator W dapat dinyatakan dengan operator U dan G, akibatnya operator W dapat dinyatakan hanya dengan operator U saja (penjelasan detail diserahkan kepada pembaca sebagai latihan).

MZI (FIF Tel-U)

LTL

November 2015

63 / 74



2


3

4

Berdasarkan de…nisi operator W dapat dinyatakan dengan operator U dan G, akibatnya operator W dapat dinyatakan hanya dengan operator U saja (penjelasan detail diserahkan kepada pembaca sebagai latihan).

Karena kita memiliki teorema yang menyatakan bahwa R adalah dual dari U, maka operator R dapat dinyatakan hanya dengan operator U saja.

MZI (FIF Tel-U)

LTL

November 2015

63 / 74

Dengan demikian himpunan fX; Ug adalah himpunan operator yang dapat merepresentasikan seluruh operator-operator temporal pada LTL. Dengan fakta yang terdapat pada logika proposisi, maka himpunan-himpunan berikut adalah adequate set of connectives untuk LTL.

MZI (FIF Tel-U)

LTL

November 2015

64 / 74

Dengan demikian himpunan fX; Ug adalah himpunan operator yang dapat merepresentasikan seluruh operator-operator temporal pada LTL. Dengan fakta yang terdapat pada logika proposisi, maka himpunan-himpunan berikut adalah adequate set of connectives untuk LTL. fX; U; :; ^g ,

MZI (FIF Tel-U)

LTL

November 2015

64 / 74

Dengan demikian himpunan fX; Ug adalah himpunan operator yang dapat merepresentasikan seluruh operator-operator temporal pada LTL. Dengan fakta yang terdapat pada logika proposisi, maka himpunan-himpunan berikut adalah adequate set of connectives untuk LTL. fX; U; :; ^g , fX; U; :; _g ,

MZI (FIF Tel-U)

LTL

November 2015

64 / 74

Dengan demikian himpunan fX; Ug adalah himpunan operator yang dapat merepresentasikan seluruh operator-operator temporal pada LTL. Dengan fakta yang terdapat pada logika proposisi, maka himpunan-himpunan berikut adalah adequate set of connectives untuk LTL. fX; U; :; ^g , fX; U; :; _g , fX; U; "g ,

MZI (FIF Tel-U)

LTL

November 2015

64 / 74

Dengan demikian himpunan fX; Ug adalah himpunan operator yang dapat merepresentasikan seluruh operator-operator temporal pada LTL. Dengan fakta yang terdapat pada logika proposisi, maka himpunan-himpunan berikut adalah adequate set of connectives untuk LTL. fX; U; :; ^g , fX; U; :; _g , fX; U; "g , fX; U; #g .

MZI (FIF Tel-U)

LTL

November 2015

64 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

65 / 74

Lampu Lalu Lintas Sederhana Asumsi yang digunakan: Model lampu lalu lintas hanya meninjau sebuah lampu lalu lintas saja (tidak berinteraksi dengan lampu lalu lintas lain). Warna yang mungkin terjadi adalah kombinasi dari merah, kuning, dan hijau. Kita akan merepresentasikan warna-warna lampu ini pada himpunan proposisi P = fred; yellow; greeng.

Permasalahan Konstruksi sebuah model LTL dengan empat state dan himpunan proposisi atom P = fred; yellow; greeng yang memenuhi spesifkasi-spesi…kasi berikut: Keamanan (safety ):

MZI (FIF Tel-U)

LTL

November 2015

66 / 74

Lampu Lalu Lintas Sederhana Asumsi yang digunakan: Model lampu lalu lintas hanya meninjau sebuah lampu lalu lintas saja (tidak berinteraksi dengan lampu lalu lintas lain). Warna yang mungkin terjadi adalah kombinasi dari merah, kuning, dan hijau. Kita akan merepresentasikan warna-warna lampu ini pada himpunan proposisi P = fred; yellow; greeng.

Permasalahan Konstruksi sebuah model LTL dengan empat state dan himpunan proposisi atom P = fred; yellow; greeng yang memenuhi spesifkasi-spesi…kasi berikut: Keamanan (safety ): 1

lampu merah, kuning, dan hijau tidak pernah menyala secara bersama-sama,

2

pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka lampu tidak boleh tiba-tiba menjadi hijau,

3

pada saat lampu lalu lintas bekerja, ketika lampu berwarna hijau, maka lampu tidak boleh tiba-tiba menjadi merah MZI (FIF Tel-U)

LTL

November 2015

66 / 74

Ketercapaian (liveness/ progress):

MZI (FIF Tel-U)

LTL

November 2015

67 / 74

Ketercapaian (liveness/ progress): 1

suatu saat lampu hijau adalah satu-satunya lampu yang menyala,

2

pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka suatu saat lampu akan berwarna hijau.

Keadilan (fairness):

MZI (FIF Tel-U)

LTL

November 2015

67 / 74


suatu saat lampu hijau adalah satu-satunya lampu yang menyala,

2

pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka suatu saat lampu akan berwarna hijau.

Keadilan (fairness): 1

lampu hijau akan menyala secara berkala (in…nitely often),

2

jika lampu merah menyala secara berkala (in…nitely often), maka lampu hijau juga menyala secara berkala (in…nitely often).

Veri…kasi dilakukan pada state s0 , di mana pada s0 hanya lampu merah saja yang menyala.

MZI (FIF Tel-U)

LTL

November 2015

67 / 74

Translasi Spesi…kasi ke Formula LTL Keamanan (safety ): 1

lampu merah, kuning, dan hijau tidak pernah menyala secara bersama-sama:

MZI (FIF Tel-U)

LTL

November 2015

68 / 74


2

lampu merah, kuning, dan hijau tidak pernah menyala secara bersama-sama: 1 := G: (red ^ yellow ^ green), pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka lampu tidak boleh tiba-tiba menjadi hijau:

MZI (FIF Tel-U)

LTL

November 2015

68 / 74


2

3

lampu merah, kuning, dan hijau tidak pernah menyala secara bersama-sama: 1 := G: (red ^ yellow ^ green), pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka lampu tidak boleh tiba-tiba menjadi hijau: 2 := G (red ! :Xgreen),

pada saat lampu lalu lintas bekerja, ketika lampu berwarna hijau, maka lampu tidak boleh tiba-tiba menjadi merah:

MZI (FIF Tel-U)

LTL

November 2015

68 / 74


2

3


pada saat lampu lalu lintas bekerja, ketika lampu berwarna hijau, maka lampu tidak boleh tiba-tiba menjadi merah: 3 := G (green ! :Xred).


suatu saat lampu hijau adalah satu-satunya lampu yang menyala:

MZI (FIF Tel-U)

LTL

November 2015

68 / 74


2

3




2

suatu saat lampu hijau adalah satu-satunya lampu yang menyala: 4 := F (green ^ :yellow ^ :red),

pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka suatu saat lampu akan berwarna hijau:

MZI (FIF Tel-U)

LTL

November 2015

68 / 74


2

3




2


pada saat lampu lalu lintas bekerja, ketika lampu berwarna merah, maka suatu saat lampu akan berwarna hijau: 5 := G (red ! Fgreen).


lampu hijau akan menyala secara berkala (in…nitely often):

MZI (FIF Tel-U)

LTL

November 2015

68 / 74


2

3




2





2

jika lampu merah menyala secara berkala (in…nitely often), maka lampu hijau juga menyala secara berkala (in…nitely often): MZI (FIF Tel-U)

LTL

6

:= GFgreen,

November 2015

68 / 74


2

3




2





2

jika lampu merah menyala secara berkala (in…nitely often), maka lampu hijau juga menyala secara berkala (in…nitely often): 7 := GFred ! GFgreen. MZI (FIF Tel-U)

LTL

6

:= GFgreen,

November 2015

68 / 74

Konstruksi Model LTL

Kita dapat mengkonstruksi model M = (S; !; L) yang ditinjau atas proposisi atom P = fred; yellow; greeng dengan 1 2

3

S = fs0 ; s1 ; s2 ; s3 g

L adalah fungsi pelabelan L : S ! 2P dengan si s0 s1 s2 s3 . L (si ) fredg fred; yellowg fgreeng fyellog ! adalah relasi transisi dengan de…nisi s0 ! s1 , s1 ! s2 , s2 ! s3 .

MZI (FIF Tel-U)

LTL

November 2015

69 / 74

MZI (FIF Tel-U)

LTL

November 2015

70 / 74

Teorema Model LTL untuk sebuah lampu lalu-lintas sederhana memenuhi spesi…kasi yang diberikan bila ditinjau pada s0 , dengan perkataan lain: M; s0 j=

i

untuk i = 1; : : : 7.

Bukti Argumen detail diserahkan kepada pembaca sebagai latihan.

MZI (FIF Tel-U)

LTL

November 2015

71 / 74

Bahasan 1


2


3


4

Sintaks Formal LTL

5

Semantik Formal LTL

6


7


8


9


MZI (FIF Tel-U)

LTL

November 2015

72 / 74

Keterkaitan LTL dengan Logika Predikat Pada penjelasan semantik untuk LTL, kita telah melihat bahwa semantik LTL yang ditinjau pada suatu lintasan (path) dapat diekspresikan dalam logika predikat. Misalnya j= F , 9i i j=

dengan domain untuk i adalah N. Kita juga dapat mengekspresikan setiap formula LTL dalam formula logika LTL yang lain. Untuk setiap proposisi atom p 2 P pada LTL, kita dapat mende…nisikan predikat Pp (t) sebagai: Pp (t) : “proposisi p benar di t” dengan domain untuk t adalah waktu (t 2 N atau t 2 N0 ). Sebagai contoh, misalkan = t1 ! t2 ! t3 ! dan untuk mempermudah kita de…nisikan t2 = t1 + 1, t3 = t2 + 1 = t1 + 2, dan secara umum tn = t1 + (n 1). Kita memiliki j=

p berarti

MZI (FIF Tel-U)

LTL

November 2015

73 / 74



j=

p berarti Pp (t1 )

T

Xp berarti

MZI (FIF Tel-U)

LTL

November 2015

73 / 74



p berarti Pp (t1 )

j=

Fp berarti

j=

Xp berarti Pp (t2 )

MZI (FIF Tel-U)

T T atau Pp (t1 + 1)

LTL

T

November 2015

73 / 74



p berarti Pp (t1 )

j=

Fp berarti 9t ((t

j=

j=

Xp berarti Pp (t2 ) Gp berarti

MZI (FIF Tel-U)

T T atau Pp (t1 + 1) t1 ) ^ Pp (t))

LTL

T

T

November 2015

73 / 74



p berarti Pp (t1 )

j=

Fp berarti 9t ((t

j=

Xp berarti Pp (t2 )

j=

Gp berarti 8t ((t

j=

pUq berarti

MZI (FIF Tel-U)

T T atau Pp (t1 + 1) t1 ) ^ Pp (t))

t1 ) ! Pp (t))

LTL

T

T T

November 2015

73 / 74



p berarti Pp (t1 )

j=

Fp berarti 9t ((t

j=

T

Xp berarti Pp (t2 )

j=

Gp berarti 8t ((t

j=

pUq berarti 9t

MZI (FIF Tel-U)

T atau Pp (t1 + 1) t1 ) ^ Pp (t))

t1 ) ! Pp (t))

(t t1 ) ^ 8t0 (t1 ^Pq (t) LTL

T

T T t0

t

1) ! Pq (t0 ) . November 2015

73 / 74

LTL Sebagai Fragmen LP yang Terputuskan (Decidable)

LTL dapat dipandang sebagai sebuah fragmen dari logika predikat orde pertama yang spesi…k dan bersifat terputuskan (decidable).

Masalah Keterpenuhan LTL (LTL Satis…ability Problem) Diberikan suatu formula LTL yang ditinjau pada model M atas proposisi P. Apakah bersifat terpenuhi (satis…able)? Masalah keterpenuhan pada LTL adalah masalah komputasi yang terputuskan (decidable). Telah dibuktikan (lihat buku teks) bahwa masalah keterpenuhan dari LTL adalah masalah dalam kelas PSPACE-complete.

MZI (FIF Tel-U)

LTL

November 2015

74 / 74

Logika Temporal Linier (Linear-Time Temporal Logic, LTL)

Recommend Documents