Часы (проверка модели)

В проверке моделей , подразделе информатики , часы — это математический объект, используемый для моделирования времени. Точнее, часы измеряют, сколько времени прошло с момента того или иного события, в этом смысле часы — это точнее абстракция секундомера . В модели некоторой конкретной программы значение часов может быть либо временем с момента запуска программы, либо временем с момента возникновения определенного события в программе. Эти часы используются в определении тактового автомата , сигнального автомата , синхронизированной пропозициональной темпоральной логики и тактовой темпоральной логики . Они также используются в таких программах, как UPPAAL , которые реализуют синхронизированные автоматы. ^[1]

Обычно модель системы использует множество часов. Эти несколько часов необходимы для отслеживания ограниченного числа событий. Все эти часы синхронизированы. Это означает, что разница в значениях двух фиксированных часов постоянна до тех пор, пока один из них не будет перезапущен. На языке электроники это означает, что джиттер часов равен нулю.

Пример

Предположим, мы хотим смоделировать лифт в десятиэтажном здании. Наша модель может иметь $n$ часы $c_{0},\dots ,c_{9}$ , такой, что значение часов $c_{i}$ это время, когда кто-то ждал лифт на этаже $i$ . Эти часы запускаются, когда кто-то вызывает лифт на этаже. $i$ (и лифт на этом этаже еще не вызывался с тех пор, как он в последний раз посещал этот этаж). Эти часы можно выключить, когда лифт прибудет на этаж. $i$ . В этом примере нам на самом деле нужно десять отдельных часов, потому что нам нужно отслеживать десять независимых событий. Еще часы $s$ может использоваться для проверки того, сколько времени лифт провел на определенном этаже.

Затем модель этого лифта может использовать эти часы, чтобы определить, удовлетворяет ли программа лифта таким свойствам, как «предположим, что лифт не удерживается на этаже более пятнадцати секунд, тогда никому не придется ждать лифта более трех минут». ". Чтобы проверить, выполняется ли это утверждение, достаточно проверить, что при каждом прогоне модели, в которой часы $s$ всегда меньше пятнадцати секунд, каждые часы $c_{i}$ выключается до достижения трех минут.

Определение

Формально набор $X$ часов — это просто конечное множество ^[1]^: 191. Каждый элемент набора часов называется часами. Интуитивно часы аналогичны переменной в логике первого порядка . Это элемент, который можно использовать в логической формуле и который может принимать несколько различных значений.

Временные оценки

Оценка часов или интерпретация часов ^[1]^: 193 $\nu$ над $X=\{x_{1},\dots ,x_{n}\}$ обычно определяется как функция от $X$ множеству неотрицательных действительных. Аналогично, оценку можно рассматривать как точку в $\mathbb {R} _{\geq 0}^{n}$ .

Первоначальное задание $\nu _{0}$ — это постоянная функция, переводящая каждые часы в 0. Интуитивно она представляет начальное время программы, когда все часы инициализируются одновременно.

Учитывая назначение часов $\nu$ и настоящий $t\geq 0$ , $\nu +t$ обозначает назначение часов, отправляющее каждые часы $x\in C$ к $\nu (x)+t$ . Интуитивно это представляет собой оценку $\nu$ после чего $t$ прошли единицы времени.

Учитывая подмножество $r\subseteq C$ часов, $\nu [r\rightarrow 0]$ обозначает присваивание, подобное $\nu$ в котором часы $r$ сбрасываются. Формально, $\nu [r\rightarrow 0]$ отправляет каждые часы $x\in r$ до 0 и каждые часы $x\not \in r$ к $\nu (x)$ .

Неактивные часы

Программа UPPAAL вводит понятие неактивных часов . ^[2] Часы неактивны в какой-то момент, если нет возможности в будущем, в котором значение часов будет проверено без предварительного сброса. В нашем примере выше часы $c_{i}$ считается неактивным, когда лифт достигает этажа $i$ , и остается неактивным, пока кто-нибудь не вызовет лифт на этаже $i$ .

Если допустить неактивные часы, оценка может связать часы $x$ какой-то особой ценности $\bot$ чтобы указать, что он неактивен. Если $\nu (x)=\bot$ затем $(\nu +t)(x)$ также равно $\bot$ .

Ограничение часов

Ограничение атомных часов — это просто термин вида $x\sim c$ , где $x$ это часы, $\sim$ — оператор сравнения, например <, ≤, = ≥ или >, и $c\in \mathbb {N}$ является интегральной константой. В нашем предыдущем примере мы можем использовать ограничения атомных часов. $c_{i}\leq 180$ заявить, что человек на этаже $i$ подождал меньше трёх минут и $s>15$ заявить, что лифт простоял на каком-то этаже более пятнадцати секунд. Оценка $\nu$ удовлетворяет оценке атомных часов $x\sim c$ тогда и только тогда, когда $\nu (x)\sim c$ .

Ограничение часов является либо конечной конъюнкцией ограничения атомных часов, либо константой «истина» (которую можно рассматривать как пустую конъюнкцию). Оценка $\nu$ удовлетворяет ограничению часов $\bigwedge _{i=1}^{n}x_{i}\sim _{i}c_{i}$ если он удовлетворяет каждому ограничению атомных часов $x_{i}\sim _{i}c_{i}$ .

Диагональное ограничение

В зависимости от контекста ограничение атомных часов также может иметь форму $x_{i}\sim x_{j}+c$ . Такое ограничение называется диагональным ограничением, поскольку $x_{1}=x_{2}+c$ определяет диагональную линию в $\mathbb {R} _{\geq 0}^{2}$ .

Разрешение диагональных ограничений может позволить уменьшить размер формулы или автомата, используемого для описания системы. Однако сложность алгоритма может увеличиться, если допускаются диагональные ограничения. В большинстве систем, использующих часы, разрешение диагонального ограничения не увеличивает выразительность логики. Теперь мы объясним, как закодировать такое ограничение с помощью логической переменной и недиагонального ограничения.

Диагональное ограничение $x_{i}\sim x_{j}+c$ может быть смоделировано с использованием недиагонального ограничения следующим образом. Когда $x_{j}$ сброшен, проверьте, $x_{i}\sim c$ держится или нет. Вызовите эту информацию в логическую переменную $b_{i,j,c}$ и заменить $x_{i}\sim x_{j}+c$ по этой переменной. Когда $x_{i}$ сбрасывается, устанавливается $b_{i,j,c}$ верно, если $\sim$ < или ≤ или если $\sim$ есть = и $c=0$ .

Способ кодирования логической переменной зависит от системы, в которой используются часы. Например, UPPAAL напрямую поддерживает логические переменные. Автоматы с таймером и сигнальные автоматы могут кодировать логическое значение в своих местоположениях. Во временной логике часов с использованием синхронизированных слов булева переменная может быть закодирована с использованием новых часов. $x_{i,j,c}$ , значение которого равно 0 тогда и только тогда, когда $b_{i,j,c}$ является ложным. То есть, $x_{i,j,c}$ сбрасывается до тех пор, пока $x_{i,j,c}$ предполагается ложным. Во временной пропозициональной темпоральной логике формула $x_{i}.\phi$ , который перезапускает $x_{i}$ а затем оценивает $\phi$ , можно заменить формулой $x_{i}.((x_{i}\sim x_{j}+c\implies \phi _{\top })\land (\neg x_{i}\sim x_{j}+c\implies \phi \bot ))$ , где $\phi _{\top }$ и $\phi _{\bot }$ являются копиями формул $\phi$ , где $x_{i}\sim x_{j}+c$ заменяются константами true и false соответственно.

Наборы, определенные ограничениями часов

Ограничение часов определяет набор оценок. В литературе рассматриваются два вида таких множеств.

Зона . — это непустой набор оценок, удовлетворяющий ограничению часов Ограничения зон и часов реализуются с использованием матрицы границ различий .

Учитывая модель $M$ , он использует конечное число констант в своих ограничениях часов. Позволять $K$ быть наибольшей используемой константой. Регион превышающих — это непустая зона, в которой нет ограничений, $K$ используются, причем такие, что минимальны для включения.

См. также

Примечания

^ Jump up to: ^а ^б ^с Алур, Раджив; Дилл, Дэвид Л. (25 апреля 1994 г.). «Теория синхронизированных автоматов» (PDF) . Теоретическая информатика . 126 (2): 183–235. дои : 10.1016/0304-3975(94)90010-8 .
^ Берманн, Герд; Дэвид, Александр; Ларсен, Ким Дж. (28 ноября 2006 г.). «Учебное пособие по Uppaal 4.0» (PDF) : 28. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

[AlurDill-1] Jump up to: ^а ^б ^с Алур, Раджив; Дилл, Дэвид Л. (25 апреля 1994 г.). «Теория синхронизированных автоматов» (PDF) . Теоретическая информатика . 126 (2): 183–235. дои : 10.1016/0304-3975(94)90010-8 .

[2] Берманн, Герд; Дэвид, Александр; Ларсен, Ким Дж. (28 ноября 2006 г.). «Учебное пособие по Uppaal 4.0» (PDF) : 28. {{cite journal}}: Для цитирования журнала требуется |journal= ( помощь )

[1]

[2]