Презентация 17 (Лекции), страница 3

. .} — множество натуральных чисел12345...Логика линейного времениСемантика формул LTLТемпоральная интерпретация LTL-формул — это модельКрипке (N, ≤, ξ), где:IIN = {1, 2, 3, . . .} — множество натуральных чисел≤ — естественный порядок на натуральных числах12345...Логика линейного времениСемантика формул LTLТемпоральная интерпретация LTL-формул — это модельКрипке (N, ≤, ξ), где:IIIN = {1, 2, 3, . .

.} — множество натуральных чисел≤ — естественный порядок на натуральных числахξ : N → 2P — оценка атомарных событий1{p}2∅3{p, q}4{p}5∅...Логика линейного времениКак можно понимать семантику формул LTL?12345{p}∅{p, q}{p}∅...Логика линейного времениКак можно понимать семантику формул LTL?12345{p}∅{p, q}{p}∅I...N = {1, 2, 3, . . .} — это состояния, через которыепоследовательно (согласно порядку ≤) проходит система впроцессе работыЛогика линейного времениКак можно понимать семантику формул LTL?12345{p}∅{p, q}{p}∅II...N = {1, 2, 3, . .

.} — это состояния, через которыепоследовательно (согласно порядку ≤) проходит система впроцессе работыоценка ξ : N → 2P указывает, какие атомарные события икогда происходят в системеЛогика линейного времениКак можно понимать семантику формул LTL?12345{p}∅{p, q}{p}∅III...N = {1, 2, 3, . . .} — это состояния, через которыепоследовательно (согласно порядку ≤) проходит система впроцессе работыоценка ξ : N → 2P указывает, какие атомарные события икогда происходят в системеLTL-формула — это утверждение о том, в какойпоследовательности происходят события PЛогика линейного времениКак можно понимать семантику формул LTL?12345{p}∅{p, q}{p}∅III...N = {1, 2, 3, .

. .} — это состояния, через которыепоследовательно (согласно порядку ≤) проходит система впроцессе работыоценка ξ : N → 2P указывает, какие атомарные события икогда происходят в системеLTL-формула — это утверждение о том, в какойпоследовательности происходят события PОсталось определить, насколько адекватно взаимосвязьсобытий в системе описывается LTL-формулойЛогика линейного времениКак можно понимать семантику формул LTL?12345{p}∅{p, q}{p}∅III...N = {1, 2, 3, . . .} — это состояния, через которыепоследовательно (согласно порядку ≤) проходит система впроцессе работыоценка ξ : N → 2P указывает, какие атомарные события икогда происходят в системеLTL-формула — это утверждение о том, в какойпоследовательности происходят события PОсталось определить, насколько адекватно взаимосвязьсобытий в системе описывается LTL-формулойДля этого определим отношение выполнимости LTL-формул втемпоральных интерпретациях: |=Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= p⇔p ∈ ξ(n)(p ∈ P)Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= p...⇔p ∈ ξ(n){.

. . , p, . . .}nn+1(p ∈ P)n+2...n+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= p...Нет: . . .⇔p ∈ ξ(n){. . . , p, . . .}nn+1S \ {p}nn+1(p ∈ P)n+2...n+k...n+2...n+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= ϕ & ψ⇔I , n |= ϕ и I , n |= ψЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= ϕ & ψ...⇔ϕ, ψnI , n |= ϕ и I , n |= ψn+1n+2...n+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IIIII , n |= ϕ & ψ ⇔ I , n |= ϕ и I , n |= ψI , n |= ϕ ∨ ψ ⇔ I , n |= ϕ или I , n |= ψI , n |= ϕ → ψ ⇔ I , n 6|= ϕ или I , n |= ψI , n |= ¬ϕ ⇔ I , n 6|= ϕЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= Xϕ⇔I , n + 1 |= ϕЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= Xϕ⇔...nI , n + 1 |= ϕϕn+1n+2...n+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:I , n |= Xϕ⇔...nНет: .

. .nIДа:I , n + 1 |= ϕϕn+1n+2¬ϕn+1n+2...n+k......n+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= Fϕ⇔существует k ≥ 0, такое что I , n + k |= ϕЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= Fϕ⇔...nсуществует k ≥ 0, такое что I , n + k |= ϕϕ......n+1n+2n+kЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= Fϕ⇔...n¬ϕnНет: .

. .существует k ≥ 0, такое что I , n + k |= ϕϕ......n+1n+2n+k¬ϕ¬ϕ¬ϕ......n+1n+2n+kЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= Gϕ⇔для любого k ≥ 0 верно I , n + k |= ϕЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= Gϕ⇔...ϕnдля любого k ≥ 0 верно I , n + k |= ϕϕϕϕ......n+1n+2n+kЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= Gϕ...Нет: .

. .⇔ϕnϕnдля любого k ≥ 0 верно I , n + k |= ϕϕϕϕ......n+1n+2n+k¬ϕϕϕ......n+1n+2n+kЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= ϕUψ⇔ существует k ≥ 0, такое что I , n + k |= ψи для любого i, 0 ≤ i < k, верно I , n + i |= ϕЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= ϕUψ...⇔ существует k ≥ 0, такое что I , n + k |= ψи для любого i, 0 ≤ i < k, верно I , n + i |= ϕϕnϕn+1ϕn+2...ψn+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= ϕRψ ⇔ либо существует k ≥ 0, такое что I , n + k |= ϕи для любого i, 0 ≤ i ≤ k, верно I , n + i |= ψ,либо для любого k ≥ 0 верно I , n + k |= ψЛогика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:IДа:I , n |= ϕRψ ⇔ либо существует k ≥ 0, такое что I , n + k |= ϕи для любого i, 0 ≤ i ≤ k, верно I , n + i |= ψ,либо для любого k ≥ 0 верно I , n + k |= ψ...ψnψn+1ψn+2...ϕ, ψn+k...Логика линейного времениСемантика формул LTLПусть I = (N, ≤, ξ) — темпоральная интерпретация (сценарийработы системы), n ∈ N (n — выбранный момент работы) и ϕ— LTL-формулаТогда отношение выполнимости I , n |= ϕ формулы ϕ винтерпретации I в момент времени n определяется так:II , n |= ϕRψ ⇔ либо существует k ≥ 0, такое что I , n + k |= ϕи для любого i, 0 ≤ i ≤ k, верно I , n + i |= ψ,либо для любого k ≥ 0 верно I , n + k |= ψДа:...ψnДа:...ψnψn+1ψn+1ψn+2ψn+2......ϕ, ψn+kψn+k......Логика линейного времениПусть ϕ — LTL-формулаЛогика линейного времениПусть ϕ — LTL-формулаОна называетсяIвыполнимой в темпоральной интерпретации I (I |= ϕ), еслиI , 1 |= ϕЛогика линейного времениПусть ϕ — LTL-формулаОна называетсяIIвыполнимой в темпоральной интерпретации I (I |= ϕ), еслиI , 1 |= ϕобщезначимой (|= ϕ), если она выполнима в любойтемпоральной интерпретацииЛогика линейного времениПусть ϕ — LTL-формулаОна называетсяIIвыполнимой в темпоральной интерпретации I (I |= ϕ), еслиI , 1 |= ϕобщезначимой (|= ϕ), если она выполнима в любойтемпоральной интерпретацииТемпоральные операторы связаны между собой определённымизаконами (равносильностями)Логика линейного времениПусть ϕ — LTL-формулаОна называетсяIIвыполнимой в темпоральной интерпретации I (I |= ϕ), еслиI , 1 |= ϕобщезначимой (|= ϕ), если она выполнима в любойтемпоральной интерпретацииТемпоральные операторы связаны между собой определённымизаконами (равносильностями)Основные такие законы приведены далееЛогика линейного времениЗаконы двойственности.I ¬Xϕ ≈ X¬ϕI ¬Fϕ ≈ G¬ϕI ¬Gϕ ≈ F¬ϕI ¬(ϕUψ) ≈ ¬ϕR¬ψI ¬(ψRϕ) ≈ ¬ϕU¬ψЛогика линейного времениЗаконы двойственности.I ¬Xϕ ≈ X¬ϕI ¬Fϕ ≈ G¬ϕI ¬Gϕ ≈ F¬ϕI ¬(ϕUψ) ≈ ¬ϕR¬ψI ¬(ψRϕ) ≈ ¬ϕU¬ψЗаконы исключения.I Fϕ ≈ ¬G¬ϕI Gϕ ≈ ¬F¬ϕI ϕUψ ≈ ¬(¬ϕR¬ψ)I ϕRψ ≈ ¬(¬ϕU¬ψ)I Fϕ ≈ true UϕI Gϕ ≈ false RϕЛогика линейного времениЗаконы двойственности.I ¬Xϕ ≈ X¬ϕI ¬Fϕ ≈ G¬ϕI ¬Gϕ ≈ F¬ϕI ¬(ϕUψ) ≈ ¬ϕR¬ψI ¬(ψRϕ) ≈ ¬ϕU¬ψЗаконы исключения.I Fϕ ≈ ¬G¬ϕI Gϕ ≈ ¬F¬ϕI ϕUψ ≈ ¬(¬ϕR¬ψ)I ϕRψ ≈ ¬(¬ϕU¬ψ)I Fϕ ≈ true UϕI Gϕ ≈ false RϕЗаконы неподвижной точки.I Fϕ ≈ ϕ ∨ XFϕI Gϕ ≈ ϕ & XGϕI ϕUψ ≈ ψ ∨ (ϕ & X(ϕUψ))I ϕRψ ≈ ψ &(ϕ ∨ X(ϕRψ))Логика линейного времениЗаконы двойственности.I ¬Xϕ ≈ X¬ϕI ¬Fϕ ≈ G¬ϕI ¬Gϕ ≈ F¬ϕI ¬(ϕUψ) ≈ ¬ϕR¬ψI ¬(ψRϕ) ≈ ¬ϕU¬ψЗаконы исключения.I Fϕ ≈ ¬G¬ϕI Gϕ ≈ ¬F¬ϕI ϕUψ ≈ ¬(¬ϕR¬ψ)I ϕRψ ≈ ¬(¬ϕU¬ψ)I Fϕ ≈ true UϕI Gϕ ≈ false RϕЗаконы неподвижной точки.I Fϕ ≈ ϕ ∨ XFϕI Gϕ ≈ ϕ & XGϕI ϕUψ ≈ ψ ∨ (ϕ & X(ϕUψ))I ϕRψ ≈ ψ &(ϕ ∨ X(ϕRψ))Доказательство.