Οι εφελκυόμενες κατασκευές από δίκτυα καλωδίων και μεμβράνες αποτελούν ένα στατικό σύστημα ανάληψης φορτίων που εκτός του ότι πετυχαίνει τη βέλτιστη αξιοποίηση της αντοχής των υλικών δίνει και φορείς μεγάλης δυσκαμψίας λόγω της διπλής καμπυλότητας των επιφανειών τους αλλά και της προέντασής τους από συγκεκριμένα όρια ή σημειακές στηρίξεις. Η εύρεση ισορροπουσών μορφών αυτών των κατασκευών δεν είναι αποτέλεσμα μόνο αρχιτεκτονικής έμπνευσης αλλά γίνεται είτε με τεχνικές φυσικής προσομοίωσης είτε ακριβέστερα με εφαρμογή αριθμητικών μεθόδων βασισμένων σε εξισώσεις ισορροπίας ή κίνησης. Στην εργασία αυτή, γίνεται διεξοδική εξέταση και μαθηματική διατύπωση της μεθόδου πυκνότητας-δύναμης προκειμένου για την εύρεση ισορροπουσών μορφών δικτύων καλωδίων και μεμβρανών ακόμα και για τις περιπτώσεις περιορισμών σχετικά με τη γεωμετρία, την εντατική κατάσταση κλπ.. Γίνεται ακόμη εξέταση των παραμέτρων που επηρεάζουν την ισορροπούσα μορφή όπως, της παραμέτρου πυκνότητας-δύναμης, της αλλαγής της θέσης των οριακών κόμβων, της τοπολογίας δικτύου και άλλων. Τέλος, προτείνεται μία διαδικασία υλοποίησης πραγματικών κατασκευών με καλώδια συγκεκριμένης διατομής και αντοχής ανάλογης με αυτή που προκύπτει από τη μέθοδο πυκνότητας-δύναμης. / Prestressed cable nets and membranes are a static load bearing system which besides achieves the optimal utilization of material strength it also gives forms of high stiffness mainly due to the existence of double curvature surfaces and prestress. Finding forms of these structures is not only a result of architectural inspiration but involves either physical modelling techniques or numerical methods based on equations of static equilibrium or motion. In this study, made a thorough examination and mathematical formulation of the force-density method which results in finding equilibrium forms for both cable nets and membranes even if restrictions regarding the geometry or stress state are included. Several types of these structures are formed in order to understand how parameters such as the force-density parameter, the nodal coordinates of fixed nodes, the network topology etc., affect the equilibrium form. Finally, it is proposed an implementation process for the construction of real structures where it is considered the self-weight of the cable net or membrane in the formfinding process.

Στη συγκεκριμένη Διατριβή μελετήσαμε την ανάλυση ευστάθειας υβριδικών δυναμικών συστημάτων τα οποία έχουν μοντελοποιηθεί με Διαφορικά Δίκτυα Petri. Τα αποτελέσματα που προτείναμε για την ανάλυση ευστάθειας χρησιμοποιούν Γραμμικές Ανισότητες Πινάκων γεγονός που τις καθιστά υπολογιστικά επιλύσιμες. Προτείναμε επίσης μια μεθοδολογία σχεδίασης ευσταθών υβριδικών συστημάτων. Χρησιμοποιήσαμε το μοντέλο Διαφορικά Δίκτυα Petri για την μοντελοποίηση δικτυακών υβριδικών συστημάτων. Προτείναμε επίσης συνθήκες ευστάθειας για διακοπτικά χρονικά καθυστερούμενα συστήματα. / In this thesis we study stability for hybrid dynamical systems modelled by Differential Petri Nets.Our stability results are formulated as Linear Matrix Inequalities in order to be computational solvable. A methodology for stabilization of hybrid dynamical systems is also introduced. The notion of Networked Hybrid System is also introduced and the model of Differential Petri Net is proposed for modelling. Stability results for switched time-dealy systems are also proposed.

A flexible workcell controller has been developed using a three level control hierarchy (workcell, workstation, equipment). The cell controller is automatically generated from a model input by the user. The model consists of three sets of graphs. One set of graphs describes the process plans of the parts produced by the manufacturing system, one set describes movements into, out of and within workstations, and the third set describes movements of parts/transporters between workstations. The controller uses an event driven Petri net to maintain state information and to communicate with lower level controllers. The control logic is contained in an artificial neural network. The Petri net state information is used as the input to the neural net and messages that are Petri net events are output from the neural net. A genetic algorithm was used to search over alternative operation choices to find a "good" solution. The system was fully implemented and several test cases are described.

In recent years, there has been much advancement in the area of verification of infinite-state systems. A system can have an infinite state-space due to unbounded data structures such as counters, clocks, stacks, queues, etc. It may also be infinite-state due to parameterization, i.e., the possibility of having an arbitrary number of components in the system. For parameterized systems, we are interested in checking correctness of all the instances in one verification step. In this thesis, we consider systems which contain both sources of infiniteness, namely: (a) real-valued clocks and (b) parameterization. More precisely, we consider two models: (a) the timed Petri net (TPN) model, which is an extension of the classical Petri net model; and (b) the timed network (TN) model in which an arbitrary number of timed automata run in parallel. We consider verification of safety properties for timed Petri nets using forward analysis. Since forward analysis is necessarily incomplete, we provide a semi-algorithm augmented with an acceleration technique in order to make it terminate more often on practical examples. Then we consider a number of problems which are generalisations of the corresponding ones for timed automata and Petri nets. For instance, we consider zenoness where we check the existence of an infinite computation with a finite duration. We also consider two variants of boundedness problem: syntactic boundedness in which both live and dead tokens are considered and semantic boundedness where only live tokens are considered. We show that the former problem is decidable while the latter is not. Finally, we show undecidability of LTL model checking both for dense and discrete timed Petri nets. Next we consider timed networks. We show undecidability of safety properties in case each component is equipped with two or more clocks. This result contrasts previous decidability result for the case where each component has a single clock. Also ,we show that the problem is decidable when clocks range over the discrete time domain. This decidability result holds when the processes have any finite number of clocks. Furthermore, we outline the border between decidability and undecidability of safety for TNs by considering several syntactic and semantic variants.

We propose in this thesis several contributions related to the quantitative verification of systems. This discipline aims to evaluate functional and performance properties of a system. Such a verification requires two ingredients: a formal model to represent the system and a temporal logic to express the desired property. Then the evaluation is done with a statistical or numerical method. The spatial complexity of numerical methods which is proportional to the size of the state space of the model makes them impractical when the state space is very large. The method of stochastic comparison with censored Markov chains is one of the methods that reduces memory requirements by restricting the analysis to a subset of the states of the original Markov chain. In this thesis we provide new bounds that depend on the available information about the chain. We introduce a new quantitative temporal logic named Hybrid Automata Stochastic Logic (HASL), for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected on-the-fly during path selection, providing the user with a powerful mean to express sophisticated measures. In essence HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. We have also developed COSMOS, a tool that implements statistical verification of HASL formulas over stochastic Petri nets. Flexible manufacturing systems (FMS) have often been modelized by Petri nets. However the modeler should have a good knowledge of this formalism. In order to facilitate such a modeling we propose a methodology of compositional modeling that is application oriented and does not require any knowledge of Petri nets by the modeler.

Siekiant maksimizuoti organizacijos pelną ir pagerinti jos veiklos rezultatus reikia efektyviai išnaudoti visus organizacijoje vykstančius verslo procesus. Tai padaryti galima naudojant įvairias verslo procesų valdymui skirtas kompiuterizuotas informacines sistemas. Projektavimo tikslas – sukurti ir aprašyti statinius ir dinaminius organizacijoje vykstančius procesus. Verslo procesams projektuoti ir analizuoti kuriant informacines sistemas, ypač jeigu jos didelės, reikia specialių projektavimo metodologijų ir priemonių, kurios šiuos procesus palengvintų, padarytų lengviau suvokiamais ir paspartintų darbą. Darbe išanalizuoti verslo procesų projektavimo būdai kuriant informacines sistemas: Petri tinklai, UML ir hibridinis Petri tinklų ir UML projektavimo metodas, pateikti jų aprašymai, savybės, galimybės. Taip pat išanalizuota organizacijose vykstantys verslo procesai. Bene daugiausia dėmesio skirta į rezultatyvumo ir žinių bei informacijos valdymo procesą, kadangi nuo jų priklauso organizacijos veiklos rezultatai. Organizacija projektuojama pradedant nuo bazinio - rezultatyvumo proceso. Todėl teorinių tyrimų aprašymo dalyje nagrinėjama pasirinkto rezultatyvumo verslo proceso projektavimas aprašytais Petri tinklų, UML bei hibridiniu metodais. Eksperimentinių tyrimų dalyje pasirinkta organizacija UAB „Proringas“, išanalizuoti joje veikiantys verslo procesai, sumodeliuotos skirtingų procesų valdymo sistemos, kurios sujungtos ir projektuotos trimis analizuojamais metodais. Metodai... [toliau žr. visą tekstą] / For maximising profit of organization and increasing its efficiency of activities must be used all business processes used in organization. The purpose of designing – to create and describe static and dynamic processes in organization. For projecting and analysing business processes while created information systems it is needed special modelling methodologies and tools that would make easier and more understandable those processes and would increase efficiency of work. There is analysed business processes design in this work while are created information systems: Petri-Net, UML and hybrid Petri-Net and UML design project methods, listed their descriptions, characteristics and possibilities. Also there are analysed business processes that take place in organization. Specialized attitude to information resources managing suppose demand of business system information, its usage and value by addressing adequate order for software. According the management position it must be coordination of data and information processing capabilities with creative person capabilities and technologies. Organization designed starting from processes and from them must be designed efficiency process. So in theoretical part it is analysed by chosen efficiency business process design described by Petri-Net and UML methods. In the part of experimental research selected organization - Joint stock company Proringas, analised business processes in it, modelled business processes that takes part in it... [to full text]

The purpose of the research is to create traffic optimal adjustment methods and algorithms based on the theory of Petri nets. To investigate the functionality of created algorithms.

In Canada, access to magnetic resonance imaging (MRI) examination is limited with an outcome of long patient waiting time. It is reported that the current median waiting time for MRI examination in Saskatoon is almost double the target for waiting time, which may aggravate the disease. This research is towards reducing the waiting time of patients for MRI examination in Canada by applying an improved management. As a first step of this effort, a comprehensive model of MRI booking and serving system is needed. The city of Saskatoon was taken as an example and the MRI booking and serving system in the city was studied. The common tools (queuing theory, system dynamics (SD) and discrete event dynamics simulation (DES)) were compared and it is found that DES is more suitable, in particular Petri nets (PNs), deemed to be the best choice for the purpose of this thesis. The model in this research was constructed on the basis of Hierarchical Coloured Petri nets (HCPNs), a combination of two extended PNs: Coloured PNs (CPNs) and Hierarchical PNs (HPNs). The model is able to simulate and predict patients' waiting times. Given that the structure of the model developed by HCPNs is still too complex, two extensions to CPNs, Ordered CPNs (OCPNs) and Prioritized HCPNs (PHCPNs), were proposed in this study to reduce the complexity of the model. Validation of the model was performed using the data of Saskatoon Health Region - Royal University Hospital. The results have shown that the proposed model can effectively describe the real system. The model has potential applications in decision-making for the selection of an optimal booking strategy to shorten waiting time and in the prediction of possible waiting time of the system in the future, which may assist MRI administrators in the management of medical resources and may greatly improve the quality of MRI service.

In this thesis, I/O signal recognizers, called VIRTUALBLOCKS, are synthesized to interface with a SYSTEM UNDER TEST (SUT). Methods for automated synthesis of virtualblocks allow us to simulate environment interfaces with SUT and also perform fault detection on SUT. Such methods must be able to recognize incoming sequences of signals from SUT, and upon the signal recognition determine the proper outgoing sequences of signals to SUT. We characterize our systems into four distinctive systems: system under test, AUXILIARY SYSTEM, controller and external environment. The auxiliary system is represented as a form of condition system Petri net (virtualblocks) and interacts with SUT along with the interaction among the controller and the external environment. Fault detection is performed by subsystems called DETECTBLOCKS synthesized from the virtualblocks. We present construction procedures for virtualblocks andamp; detectblocks and discuss the notion of LEGALITY and DETECTABILITY. Finally, we illustrate our approach using a model of a scanner control unit.

The current thesis considers the issue of state estimation of condition systems, a form of petri net with signal inputs and outputs. In previous research the problem of unobservability due to progress confusion was identified, in the presence of which state estimation is not possible. Here we introduce the notion of Time Condition Systems", a class of condition systems that uses timing information from condition models to overcome state estimation problem caused by progress confusion. To make use of the timing information in the plant model, a procedure called Exploded Time Plant" is synthesized. This procedure makes the plant model an observable model. It is proved that this procedure does not alter the structural and temporal behavior of the plant model and the plant maintains its integrity. The time plant(s) and the corresponding Exploded time plant(s) are subsequently used to develop observer(s) and controller(s) for Time condition models.