PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 7

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  automat czasowy
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Diagnosis of hybrid systems through bond graph, observers and timed automata
Mhamdi Lotfi, Achbi Mohammed Said, Dhouibi Hedi, Kechida Sihem
Diagnostyka
|
2020
|
Vol. 21, No. 3
113--125
EN
Despite technological advances and progress in industrial systems, the fault diagnosis of a system remains a very important task. In fact an effective diagnosis contributes not only to improved reliability but also to a decrease in maintenance costs. This paper presents an approach to a diagnosis of hybrid systems thanks to the use of Bond Graphs, Observer and Timed Automata. Dynamic models (in normal and failing mode) are generated by an observer based methods as well as through state equations generated by the Bond Graphs model. The procedure of fault localization through a method based on the observer does not allow locating faults with the same signature of failure. Thus the diagnosis technique for the localization of these defects will be based on the time analysis using Timed Automata. The proposed approach is then validated by simulation tests in a two tanks hydraulic system.
2
Content available SAT-based searching for k-quasi-optimal runs in weighted timed automata
Woźna-Szcześniak B., Zbrzezny A.
Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
|
2010
|
Vol. 15
163--176
EN
In the paper we are concerned with an optimal cost reachability problem for weighted timed automata, and we use a translation to SAT to solve the problem. In particular, we show how to find a run of length k ∈ IN that starts at the initial state and terminates at a state containing a target location, its total cost belongs to the interval [c,c+1), for some natural number c ∈ IN, and the cost of each other run of length k, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of runs is called k-quasi-optimal. We exemplify the use of our solution to the mentioned problem by means of the air traffic control problem, and we provide some preliminary experimental results.
3
Content available remote A Boolean Encoding of Arithmetic Operations
Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2007
|
Nr 999
1-35
EN
In this paper we present algorithms for a~Boolean encoding of four basic arithmetic operations on integer numbers: addition, subtraction, multiplication and division. Integer numbers are encoded in two's complement system as vectors of Boolean formulas and arithmetic operations are faithfully encoded as operations on vectors of Boolean formulas. In addition, we also provide an algorithm for a Boolean encoding of the operations of calculating integer square root and an algorithm for a Boolean encoding of the operation of exponentiation with nonnegative integer exponent.
PL
W pracy przedstawiamy algorytmy realizujące Boolowskie kodowanie czterech podstawowych operacji arytmetycznych: dodawania, odejmowania, mnożenia i dzielenia. Liczby całkowite są kodowane w systemie uzupełnieniowym do 2 jako wektory formuł Boolowskich a operacje arytmetyczne są zakodowane jako operacje na wektorach formuł Boolowskich. Dodatkowo przedstawiamy algorytmy realizujące Boolowskie kodowanie dla operacji obliczania całkowitego pierwiastka kwadratowego oraz dla operacji potęgowania.
4
Content available Timed concurrent state machines
Daszczuk W. B.
Computer Science
|
2007
|
Vol. 8, Spec. Ed
23-36
EN
Timed Concurrent State Machines are an application of Alur Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to storę a verified system in ready-to-verification form, and to multiply it by various testing automata.
PL
Współbieżne maszyny stanowe z czasem TCSM są aplikacją automatów czasowych Alura w środowisku koincydencyjnym współbieżnych maszyn czasowych CSM (w przeciwieństwie do środowisk przeplotowych). TCSM pasują do idei automatów testujących, które pozwalają wyspecyfikować zależności czasowe łatwiej niż poprzez formuły temporalne. Ponadto zdefiniowano sposób wyznaczania globalnej przestrzeni stanów w dziedzinie czasu (współbieżne maszyny stanowe regionów RCSM), co pozwala przechowywać badany system w postaci gotowej do weryfikacji i mnożyć go przez różne automaty testujące.
5
Content available remote Slicing of Timed Automata with Discrete Data
Janowska A., Janowski P.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2006
|
Nr 990
1-29
EN
The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic CTL_X*
PL
Praca przedstawia zastosowanie analizy statycznej do uzyskania abstrakcyjnego modelu systemu. Proponowana metoda jest oparta na technice plastrowania programów. Analizie podlega system przedstawiony jako zbiór automatów czasowych rozszerzonych o dane dyskretne, który to formalizm jest stosowany przez weryfikatory modelowe dla systemów czasowych. W przedstawionej metodzie abstrakcja systemu zachowuje prawdziwość formuł logiki temporalnej CTL_X* i jest uzalezniona od weryfikowanej własności.
6
Content available remote SAT-Based Bounded Model Checking for the Universal Fragment of TCTL
Penczek W., Woźna B., Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 947
1-26
EN
Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.
PL
Ograniczona Weryfikacja Modelowa, bzaująca na metodach SAT, polega na poszukiwaniu kontrprzykładów o długości ograniczonej przez pewną liczbę całkowitą k > 0 oraz generowanie formuły zdaniowej, która jest spełniana wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla automatów czasowych reprezentowanych przez siec współbieżnych i wzajemnie komunikujących się komponentów oraz własności wyrażanych w języku logiki TACTL (uniwersalnego fragmentu TCTL).
7
Content available remote Checking Reachability Properties for Timed Automata via SAT
Woźna B., Penczek W., Zbrzezny A.
Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
|
2002
|
Nr 949
1-19
EN
The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded to the depth k Î N and encoded as a prepositional formula. Next the desired property is translated to a prepositional formula and the satisfiability of the conjunction of the two above defined formulas is checked. The unfolding of the transition can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results. Keywords : Reachability problem, bounded model checking, translation to SAT, Timed Automata, Augmented Region Graphs, discretization.
PL
Testowanie osiągalności automatów czasowych z wykorzystaniem SAT. Praca opisuje nowe podejście do problemu osiągalności dla automatów czasowych. Główna idea polega na połączeniu znanego algorytmu przeszukującego przestrzeń stanów wszerz metodą BFS oraz metody ograniczonej weryfikacji modelowej. Aby sprawdzić, czy stan spełniający daną własność jest osiągalny w modelu dla rozważanego automatu czasowego postępujemy następująco. Rozwijamy stopniowo relację przejścia dla automatu, aż do głębokości k Î N i kodujemy ją jako formułę zdaniową. Następnie, za pomocą formuły zdaniowej kodowana jest rozważana własność i sprawdzana jest spełnialność koniunkcji obydwu zdefiniowanych formuł zdaniowych. Rozwijanie relacji przejścia może zostać zakończone jeśli poszukiwany stan został znaleziony lub wszystkie stany danego automatu czasowego zostały przeszukane.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.