Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: ATL

Sortuj według:

Ogranicz wyniki do:

Unbounded Model Checking for ATL

Kański Michał, Niewiadomski Artur, Kacprzak Magdalena, Penczek Wojciech, Nabiałek Wojciech

Studia Informatica : systems and information technology

2021

Vol. 1-2(25)

5--22

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

Underapproximating ATL with Imperfect Information and Imperfect Recall

Jamroga W., Knapik M.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2015

Nr 1032

1--16

We investigate the correspondence between model checking of af-AMCi and ATLir , on the example of reachability. We identify some of the reasons for the fact that these logics are of uncomparable expressivity. These observations form the basis for a novel method for underapproximating ATLir by means of fixed-point calculations. We introduce a special version of the next-step operator, called Persistent Imperfect Next-Step Operator h_iF and show how it can be used to define a new version of reachability that carries to ATLir.

W pracy badane są związki pomiędzy weryfikacją modelową Bezpamięciowej Logiki Temporalnej Czasu Alternującego z Niepełną Informacją ATLir i Epistemicznego Alternującego Mu-Rachunku af-AMCi. Jak pokazano, naturalne uogólnienia pojęcia osiągalności z ATLir -a do af-AMCi nie przynoszą dobrych efektów: osiągalność w af-AMCi nie pociąga za sobą osiągalności w ATLir . Po zidentyfikowaniu części powodów, dla których tak się dzieje, zaproponowano nową wersję operatora następnego kroku, który pozwala na przybliżanie osiągalności w ATLir przy pomocy obliczeń stałopunktowych.

Wytwarzanie serwisów informacyjnych z wykorzystaniem koncepcji modelowania dziedzin : budowa transformacji

Kosior A., Stasiak A., Dąbrowski W.

Biuletyn Instytutu Automatyki i Robotyki

2012

R. 18, nr 32

53-83

W artykule przedstawiono klasyfikację transformacji modeli (M2M, M2T, T2M, JET) oraz modeli mapowań. Szczegółowo omówiono proces wytwarzania generycznych mechanizmów transformacji umożliwiających wielokrotne przekształcenia modeli. Dodatkowo zaprezentowano przykładowe transformacje opracowane w ramach projektu serwisu informacyjnego.

The paper presents a classification of models transformations (M2M, M2T, T2M, JET) and mapping models. The process of producing generic transformation mechanisms allowing to multiple models transformations is discussed in details. In addition, examples of transformations are presented within the information service project.