Экспериментальное исследование.
Модель вероятностных многоагентных систем и их верификация
Указанные выше алгоритмы были реализованы в программе PMASVerification, которая содержит следующие основные компоненты: Автор благодарен М. И. Дехтярю за постановку задачи и внимание к работе и М. К. Валиеву за полезные замечания. Начнем со сравнения времени вычисления оператора X с его аналогом, выраженным через оператор X. Таблица 1 показывает, что использование оператора X существенно… Читать ещё >
Экспериментальное исследование. Модель вероятностных многоагентных систем и их верификация (реферат, курсовая, диплом, контрольная)
Указанные выше алгоритмы были реализованы в программе PMASVerification, которая содержит следующие основные компоненты:
- · Редактор ВМАС позволяет задавать и редактировать все данные, задающие ВМАС.
- · Транслятор ВМАС в цепь Маркова реализует алгоритм TranslateMarkovChain.
- · Редактор формул темпоральной логики позволяет вводить и редактировать формулы, задающие проверяемые свойства ВМАС.
- · Верификатор реализует алгоритм вычисления вероятностей формул PTL+ X[k].
Ниже в таблицах представлены некоторые результаты экспериментов с программой PMASVerification. Определялось время работы в мсек программы верификации цепи Маркова в зависимости от сложности верифицируемой формулы, числа состояний цепи и процента количества дуг в среднем из одного состояния по отношению к общему числу состояний (например, если в таблице указано 10% процентов дуг, а всего состояний 1000, то из каждого состояния в среднем выходит 100 дуг). Вероятности переходов и начальное распределение, а также значения пропозициональных переменных на состояниях задавались случайно. Верифицируемые формулы имеют вид:
- · (x1 U x2)
- · (x1 U x2) & (x3 U x4)
- · (x1 U x2) & (x3 U x4) & (x5 U x6)
- · X x1
- · X x1 & X x2
- · X x1 & X x2 & X x3
Начнем со сравнения времени вычисления оператора X[3] с его аналогом, выраженным через оператор X.
Табл. 1. Формулы с оператором X[k] (1% дуг).
Состояния. | X[3](x1). | XXX (x1) v XX (x1) v X (x1). | |
Таблица 1 показывает, что использование оператора X[k] существенно сокращает время вычисления.
Табл. 2. Формулы с оператором U (1% дуг).
Состояния. | 1 оператор | 2 оператора. | 3 оператора. | |
Табл. 3. Формулы с оператором X (1% дуг).
Состояния. | 1 оператор | 2 оператора. | 3 оператора. | |
Табл. 4. Формулы с оператором U (10% дуг).
Состояния. | 1 оператор | 2 оператора. | 3 оператора. | |
Табл. 5. Формулы с оператором X (10% дуг).
Состояния. | 1 оператор | 2 оператора. | 3 оператора. | |
Таблицы 2 — 5 показывают, что формулы, содержащие только X, верифицируются существенно быстрее формул с тем же числом операторов U, но во всех случаях усложнение формулы приводит к быстрому (теоретически экспоненциальному) росту времени ее верификации. Увеличение «плотности» цепи Маркова также приводит к почти линейному росту времени верификации.
Благодарности
Автор благодарен М. И. Дехтярю за постановку задачи и внимание к работе и М. К. Валиеву за полезные замечания.