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

данные на принтер всегда передаёт не более чем одинкомпьютерВерификация распределённых системКорректное взаимодействие компьютеров с принтеромудовлетворяет следующим требованиям:1. данные на принтер всегда передаёт не более чем одинкомпьютер2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занятВерификация распределённых системКорректное взаимодействие компьютеров с принтеромудовлетворяет следующим требованиям:1.

данные на принтер всегда передаёт не более чем одинкомпьютер2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занят3. если принтер оказался занят, то он рано или поздноприступит к печатиВерификация распределённых системКорректное взаимодействие компьютеров с принтеромудовлетворяет следующим требованиям:1. данные на принтер всегда передаёт не более чем одинкомпьютер2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занят3. если принтер оказался занят, то он рано или поздноприступит к печати4.

принтер, завершивший печать, обязательно освободитсяВерификация распределённых системКорректное взаимодействие компьютеров с принтеромудовлетворяет следующим требованиям:1. данные на принтер всегда передаёт не более чем одинкомпьютер2. если принтер свободен и какой-либо компьютер собираетсяпередать данные на печать, то рано или поздно принтерокажется занят3. если принтер оказался занят, то он рано или поздноприступит к печати4. принтер, завершивший печать, обязательно освободитсяА ещё?Верификация распределённых системКак можно формально записать такого рода свойства?Верификация распределённых системКак можно формально записать такого рода свойства?В распределённой системе с течением времени происходят(протекают) некоторые события: приём/пересылка сообщений,печать, изменение состояний данных, бездействие, .

. .Верификация распределённых системКак можно формально записать такого рода свойства?В распределённой системе с течением времени происходят(протекают) некоторые события: приём/пересылка сообщений,печать, изменение состояний данных, бездействие, . . .Каждое событие event можно охарактеризоватьпропозициональной переменной pevent :pevent = true ⇔ происходит событие eventВерификация распределённых системКак можно формально записать такого рода свойства?В распределённой системе с течением времени происходят(протекают) некоторые события: приём/пересылка сообщений,печать, изменение состояний данных, бездействие, .

. .Каждое событие event можно охарактеризоватьпропозициональной переменной pevent :pevent = true ⇔ происходит событие eventСобытия начинаются и завершаются со временемВерификация распределённых системКак можно формально записать такого рода свойства?В распределённой системе с течением времени происходят(протекают) некоторые события: приём/пересылка сообщений,печать, изменение состояний данных, бездействие, . . .Каждое событие event можно охарактеризоватьпропозициональной переменной pevent :pevent = true ⇔ происходит событие eventСобытия начинаются и завершаются со временемЗначит, нужны средства описания времениВерификация распределённых системКак можно формально записать такого рода свойства?В распределённой системе с течением времени происходят(протекают) некоторые события: приём/пересылка сообщений,печать, изменение состояний данных, бездействие, .

. .Каждое событие event можно охарактеризоватьпропозициональной переменной pevent :pevent = true ⇔ происходит событие eventСобытия начинаются и завершаются со временемЗначит, нужны средства описания времениТакие средства есть в темпоральных логикахВерификация распределённых системКак можно формально записать такого рода свойства?В распределённой системе с течением времени происходят(протекают) некоторые события: приём/пересылка сообщений,печать, изменение состояний данных, бездействие, . .

.Каждое событие event можно охарактеризоватьпропозициональной переменной pevent :pevent = true ⇔ происходит событие eventСобытия начинаются и завершаются со временемЗначит, нужны средства описания времениТакие средства есть в темпоральных логикахСосредоточим внимание на логике линейного времени:(Linear Temporal Logic)LTLЛогика линейного времениКакими средствами располагает LTL?Логика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийЛогика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийЛогика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийIтемпоральные операторы для описания времени:Логика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийIтемпоральные операторы для описания времени:IX (neXt time): “в следующий момент времени”Логика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийIтемпоральные операторы для описания времени:IIX (neXt time): “в следующий момент времени”F (in Future): “когда-нибудь в будущем”Логика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийIтемпоральные операторы для описания времени:IIIX (neXt time): “в следующий момент времени”F (in Future): “когда-нибудь в будущем”G (Globally): “всегда в будущем”Логика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийIтемпоральные операторы для описания времени:IIIIX (neXt time): “в следующий момент времени”F (in Future): “когда-нибудь в будущем”G (Globally): “всегда в будущем”U (Until): “до тех пор пока”Логика линейного времениКакими средствами располагает LTL?Iпропозициональные переменные для описанияпримитивных (атомарных) событийIлогические связки (&, ∨, →, ¬) для описания составныхсобытийIтемпоральные операторы для описания времени:IIIIIX (neXt time): “в следующий момент времени”F (in Future): “когда-нибудь в будущем”G (Globally): “всегда в будущем”U (Until): “до тех пор пока”R (Release): “освободить событие”Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийЛогика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:Ip(p ∈ P)Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIp(ϕ & ψ)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(p ∈ P)(ϕ, ψ — события)Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIIp(p ∈ P)(ϕ & ψ)(ϕ, ψ — события)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(Xϕ)“в следующий момент произойдёт ϕ”Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIIIp(p ∈ P)(ϕ & ψ)(ϕ, ψ — события)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(Xϕ)“в следующий момент произойдёт ϕ”(Fϕ)“когда-нибудь в будущем произойдёт ϕ”Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIIIIp(p ∈ P)(ϕ & ψ)(ϕ, ψ — события)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(Xϕ)“в следующий момент произойдёт ϕ”(Fϕ)“когда-нибудь в будущем произойдёт ϕ”(Gϕ)“всегда в будущем будет происходить ϕ”Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIIIIIp(p ∈ P)(ϕ & ψ)(ϕ, ψ — события)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(Xϕ)“в следующий момент произойдёт ϕ”(Fϕ)“когда-нибудь в будущем произойдёт ϕ”(Gϕ)“всегда в будущем будет происходить ϕ”(ϕUψ)“ψ обязательно произойдёт,а до тех пор будет протекать ϕ”Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIIIIIIp(p ∈ P)(ϕ & ψ)(ϕ, ψ — события)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(Xϕ)“в следующий момент произойдёт ϕ”(Fϕ)“когда-нибудь в будущем произойдёт ϕ”(Gϕ)“всегда в будущем будет происходить ϕ”(ϕUψ)“ψ обязательно произойдёт,а до тех пор будет протекать ϕ”(ϕRψ)“пока ϕ не произошло, ψ не может завершиться”Логика линейного времениСинтаксис формул LTLПусть P — множество пропозициональных переменных, илиатомарных событийТогда LTL-формулами (или событиями) являются:IIIIIIIIp(p ∈ P)(ϕ & ψ)(ϕ, ψ — события)(ϕ ∨ ψ), (ϕ → ψ), (¬ϕ)(Xϕ)“в следующий момент произойдёт ϕ”(Fϕ)“когда-нибудь в будущем произойдёт ϕ”(Gϕ)“всегда в будущем будет происходить ϕ”(ϕUψ)“ψ обязательно произойдёт,а до тех пор будет протекать ϕ”(ϕRψ)“пока ϕ не произошло, ψ не может завершиться”Приоритет операций: X, F, G, ¬; затем U, R;затем остальные связки с обычным приоритетомЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Логика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:Логика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:Iкогда-нибудь Даша полюбит СашуЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:Iкогда-нибудь Даша полюбит Сашу: FpЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить СашуЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpДаша будет любить Сашу, пока не полюбит ПашуЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpДаша будет любить Сашу, пока не полюбит ПашуGp ∨ pUqЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIIIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpДаша будет любить Сашу, пока не полюбит ПашуGp ∨ pUqДаша постоянно будет влюбляться в ПашуЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIIIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpДаша будет любить Сашу, пока не полюбит ПашуGp ∨ pUqДаша постоянно будет влюбляться в ПашуGFqЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIIIIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpДаша будет любить Сашу, пока не полюбит ПашуGp ∨ pUqДаша постоянно будет влюбляться в ПашуGFqесли Даша влюбится в Пашу, то никогда не разлюбитЛогика линейного времениПримерРассмотрим два атомарных события:p: “Даша любит Сашу”q: “Даша любит Пашу”Тогда можно записать, например, такие составные события:IIIIIкогда-нибудь Даша полюбит Сашу: FpДаша всегда будет любить Сашу: GpДаша будет любить Сашу, пока не полюбит ПашуGp ∨ pUqДаша постоянно будет влюбляться в ПашуGFqесли Даша влюбится в Пашу, то никогда не разлюбитG(q → Gq)Логика линейного времениСемантика формул LTLЛогика линейного времениСемантика формул LTLТемпоральная интерпретация LTL-формул — это модельКрипке (N, ≤, ξ)Логика линейного времениСемантика формул LTLТемпоральная интерпретация LTL-формул — это модельКрипке (N, ≤, ξ), где:IN = {1, 2, 3, .