Global ETD Search

1	On bisimulation and model-checking for concurrent systems with partial order semantics Gutierrez, Julian January 2011 (has links) In concurrency theory—the branch of (theoretical) computer science that studies the logical and mathematical foundations of parallel computation—there are two main formal ways of modelling the behaviour of systems where multiple actions or events can happen independently and at the same time: either with interleaving or with partial order semantics. On the one hand, the interleaving semantics approach proposes to reduce concurrency to the nondeterministic, sequential computation of the events the system can perform independently. On the other hand, partial order semantics represent concurrency explicitly by means of an independence relation on the set of events that the system can execute in parallel; following this approach, the so-called ‘true concurrency’ approach, independence or concurrency is a primitive notion rather than a derived concept as in the interleaving framework. Using interleaving or partial order semantics is, however, more than a matter of taste. In fact, choosing one kind of semantics over the other can have important implications—both from theoretical and practical viewpoints—as making such a choice can raise different issues, some of which we investigate here. More specifically, this thesis studies concurrent systems with partial order semantics and focuses on their bisimulation and model-checking problems; the theories and techniques herein apply, in a uniform way, to different classes of Petri nets, event structures, and transition system with independence (TSI) models. Some results of this work are: a number of mu-calculi (in this case, fixpoint extensions of modal logic) that, in certain classes of systems, induce exactly the same identifications as some of the standard bisimulation equivalences used in concurrency. Secondly, the introduction of (infinite) higher-order logic games for bisimulation and for model-checking, where the players of the games are given (local) monadic second-order power on the sets of elements they are allowed to play. And, finally, the formalization of a new order-theoretic concurrent game model that provides a uniform approach to bisimulation and model-checking and bridges some mathematical concepts in order theory with the more operational world of games. In particular, we show that in all cases the logic games for bisimulation and model-checking developed in this thesis are sound and complete, and therefore, also determined—even when considering models of infinite state systems; moreover, these logic games are decidable in the finite case and underpin novel decision procedures for systems verification. Since the mu-calculi and (infinite) logic games studied here generalise well-known fixpoint modal logics as well as game-theoretic decision procedures for analysing concurrent systems with interleaving semantics, this thesis provides some of the groundwork for the design of a logic-based, game-theoretic framework for studying, in a uniform manner, several concurrent systems regardless of whether they have an interleaving or a partial order semantics. 004.01
2	Complexité dans les Jeux Infinis sur les Graphes et les Réseaux de Contraintes Temporelles / Complexity in Infinite Games on Graphs and Temporal Constraint Networks Comin, Carlo 20 March 2017 (has links) Cette thèse porte sur un certain nombre de problèmes algorithmiques motivés par la planification temporelle automatisée et la vérification formelle des systèmes réactifs et finis. Nous nous sommes concentrés sur les méthodes théoriques des jeux pour obtenir de nouvelles connaissances, des limites de complexité améliorées et des algorithmes plus rapides pour les modèles suivants: réseaux temporels hyper, réseaux conditionnels Simples / Hyper temporels, jeux de mise à jour, jeux Muller McNaughton et jeux Mean Payoff / This dissertation deals with a number of algorithmic problems motivated by automated temporal planning and formal verification of reactive and finite state systems. We focused on game theoretical methods to obtain novel insights, improved complexity bounds, and faster algorithms for the following models: Hyper Temporal Networks, Conditional Simple/Hyper Temporal Networks, Update Games, Muller McNaughton Games, and Mean Payoff Games Algorithmics Complexité Computationnelle Jeux Infinis Réseaux de Contraintes Temporelles Algorithmics Computational Complexity Infinite Games Temporal Constraint Networks
3	Combinatorial Optimization for Infinite Games on Graphs Björklund, Henrik January 2005 (has links) Games on graphs have become an indispensable tool in modern computer science. They provide powerful and expressive models for numerous phenomena and are extensively used in computer- aided verification, automata theory, logic, complexity theory, computational biology, etc. The infinite games on finite graphs we study in this thesis have their primary applications in verification, but are also of fundamental importance from the complexity-theoretic point of view. They include parity, mean payoff, and simple stochastic games. We focus on solving graph games by using iterative strategy improvement and methods from linear programming and combinatorial optimization. To this end we consider old strategy evaluation functions, construct new ones, and show how all of them, due to their structural similarities, fit into a unifying combinatorial framework. This allows us to employ randomized optimization methods from combinatorial linear programming to solve the games in expected subexponential time. We introduce and study the concept of a controlled optimization problem, capturing the essential features of many graph games, and provide sufficent conditions for solvability of such problems in expected subexponential time. The discrete strategy evaluation function for mean payoff games we derive from the new controlled longest-shortest path problem, leads to improvement algorithms that are considerably more efficient than the previously known ones, and also improves the efficiency of algorithms for parity games. We also define the controlled linear programming problem, and show how the games are translated into this setting. Subclasses of the problem, more general than the games considered, are shown to belong to NP intersection coNP, or even to be solvable by subexponential algorithms. Finally, we take the first steps in investigating the fixed-parameter complexity of parity, Rabin, Streett, and Muller games. infinite games combinatorial optimization randomized algorithms model checking strategy evaluation functions linear programming iterative improvement local search Computer science Datavetenskap
4	Aplikace deskriptivní teorie množin v matematické analýze / Applications of descriptive set theory in mathematical analysis Doležal, Martin January 2013 (has links) We characterize various types of σ-porosity via an infinite game in terms of winning strategies. We use a modification of the game to prove and reprove some new and older in- scribing theorems for σ-ideals of σ-porous type in locally compact metric spaces. We show that there exists a closed set which is σ-(1 − ε)-symmetrically porous for every 0 < ε < 1 but which is not σ-1-symmetrically porous. Next, we prove that the realizable by an action unitary representations of a finite abelian group Γ on an infinite-dimensional complex Hilbert space H form a comeager set in Rep(Γ, H). 1
5	Combinatorial Optimization for Infinite Games on Graphs Björklund, Henrik January 2005 (has links) <p>Games on graphs have become an indispensable tool in modern computer science. They provide powerful and expressive models for numerous phenomena and are extensively used in computer- aided verification, automata theory, logic, complexity theory, computational biology, etc.</p><p>The infinite games on finite graphs we study in this thesis have their primary applications in verification, but are also of fundamental importance from the complexity-theoretic point of view. They include parity, mean payoff, and simple stochastic games.</p><p>We focus on solving graph games by using iterative strategy improvement and methods from linear programming and combinatorial optimization. To this end we consider old strategy evaluation functions, construct new ones, and show how all of them, due to their structural similarities, fit into a unifying combinatorial framework. This allows us to employ randomized optimization methods from combinatorial linear programming to solve the games in expected subexponential time.</p><p>We introduce and study the concept of a controlled optimization problem, capturing the essential features of many graph games, and provide sufficent conditions for solvability of such problems in expected subexponential time.</p><p>The discrete strategy evaluation function for mean payoff games we derive from the new controlled longest-shortest path problem, leads to improvement algorithms that are considerably more efficient than the previously known ones, and also improves the efficiency of algorithms for parity games.</p><p>We also define the controlled linear programming problem, and show how the games are translated into this setting. Subclasses of the problem, more general than the games considered, are shown to belong to NP intersection coNP, or even to be solvable by subexponential algorithms.</p><p>Finally, we take the first steps in investigating the fixed-parameter complexity of parity, Rabin, Streett, and Muller games.</p> Datavetenskap infinite games combinatorial optimization randomized algorithms model checking strategy evaluation functions linear programming iterative improvement local search Datavetenskap Computer science Datavetenskap
6	Games and Probabilistic Infinite-State Systems Sandberg, Sven January 2007 (has links) <p>Computer programs keep finding their ways into new safety-critical applications, while at the same time growing more complex. This calls for new and better methods to verify the correctness of software. We focus on one approach to verifying systems, namely that of <i>model checking</i>. At first, we investigate two categories of problems related to model checking: <i>games</i> and <i>stochastic infinite-state systems</i>. In the end, we join these two lines of research, by studying <i>stochastic infinite-state games</i>.</p><p>Game theory has been used in verification for a long time. We focus on finite-state 2-player parity and limit-average (mean payoff) games. These problems have applications in model checking for the <i>μ</i>-calculus, one of the most expressive logics for programs. We give a simplified proof of memoryless determinacy. The proof applies <i>both</i> to parity and limit-average games. Moreover, we suggest a strategy improvement algorithm for limit-average games. The algorithm is discrete and strongly subexponential.</p><p>We also consider probabilistic infinite-state systems (Markov chains) induced by three types of models. <i>Lossy channel systems (LCS)</i> have been used to model processes that communicate over an unreliable medium. <i>Petri nets</i> model systems with unboundedly many parallel processes. <i>Noisy Turing machines</i> can model computers where the memory may be corrupted in a stochastic manner. We introduce the notion of <i>eagerness</i> and prove that all these systems are eager. We give a scheme to approximate the value of a reward function defined on paths. Eagerness allows us to prove that the scheme terminates. For probabilistic LCS, we also give an algorithm that approximates the limit-average reward. This quantity describes the long-run behavior of the system.</p><p>Finally, we investigate Büchi games on probabilistic LCS. Such games can be used to model a malicious cracker trying to break a network protocol. We give an algorithm to solve these games.</p> program verification model checking determinacy strategy improvement infinite games parity games mean payoff games stochastic games Büchi games reachability games limiting average limiting behavior Markov chains infinite-state systems lossy channel systems vector addition systems noisy Turing machines Computer science Datavetenskap
7	Games and Probabilistic Infinite-State Systems Sandberg, Sven January 2007 (has links) Computer programs keep finding their ways into new safety-critical applications, while at the same time growing more complex. This calls for new and better methods to verify the correctness of software. We focus on one approach to verifying systems, namely that of model checking. At first, we investigate two categories of problems related to model checking: games and stochastic infinite-state systems. In the end, we join these two lines of research, by studying stochastic infinite-state games. Game theory has been used in verification for a long time. We focus on finite-state 2-player parity and limit-average (mean payoff) games. These problems have applications in model checking for the μ-calculus, one of the most expressive logics for programs. We give a simplified proof of memoryless determinacy. The proof applies both to parity and limit-average games. Moreover, we suggest a strategy improvement algorithm for limit-average games. The algorithm is discrete and strongly subexponential. We also consider probabilistic infinite-state systems (Markov chains) induced by three types of models. Lossy channel systems (LCS) have been used to model processes that communicate over an unreliable medium. Petri nets model systems with unboundedly many parallel processes. Noisy Turing machines can model computers where the memory may be corrupted in a stochastic manner. We introduce the notion of eagerness and prove that all these systems are eager. We give a scheme to approximate the value of a reward function defined on paths. Eagerness allows us to prove that the scheme terminates. For probabilistic LCS, we also give an algorithm that approximates the limit-average reward. This quantity describes the long-run behavior of the system. Finally, we investigate Büchi games on probabilistic LCS. Such games can be used to model a malicious cracker trying to break a network protocol. We give an algorithm to solve these games. program verification model checking determinacy strategy improvement infinite games parity games mean payoff games stochastic games Büchi games reachability games limiting average limiting behavior Markov chains infinite-state systems lossy channel systems vector addition systems noisy Turing machines Computer science Datavetenskap
8	Learning, Improvisation, and Identity Expansion in Innovative Organizations Keidan, Joshua January 2020 (has links) No description available. Adult Education Behavioral Sciences Business Administration Business Education Design Education Education Philosophy Education Policy Educational Leadership Educational Sociology Educational Theory Entrepreneurship Higher Education Inservice Training Instructional Design Management Multicultural Education Vocational Education Theater Studies Teaching Teacher Education Systems Design Social Structure Sociology Social Psychology Secondary Education Psychology Organization Theory learning improvisation identity change identity expansion innovation innovative organizations learning organizations well-being Vygotsky infinite games joy fear ownership self-directed learning student-centered learning business

Search results