Real time systems distinguish themselves by explicitly stating timing constraints in the system specification. This requires specific methods and tools in system design to ensure such constraints. We focus on one of the methods applied in the validation phase, namely formal verification. This method automatically establishes correctness of the system model with mathematical rigor. In order to apply mechanical procedures to determine whether the system satisfies the requirements, we first have to model the validated part of the system in a mathematical form. This thesis deals with one such formalism - timed automata - and investigates different types of infinite state structures arising in the verification procedures related to this formalism. There are two different views which open the door for introduction of such structures. First, we turn outwards and extend timed automata with additional infinite data structures - unbounded queues. These queues serve different purposes. In one case, the queues contain computation tasks and, together with a timed automaton, model a real-time system with tasks. The problem of interest in this setting is schedulability analysis. We investigate the decidability boundary in presence of various features such as preemption, variable computation times of tasks, and communication between the timed automaton and the task queue. In the other case, we use queues for asynchronous communication between timed automata running synchronously in parallel. These queues store messages issued by one automaton and waiting to be read by another automaton. Such situations occur among other cases in real-time control systems where several concurrently running tasks communicate via buffers. We study the decidability border for reachability analysis depending on various communication topologies of these systems. Secondly, we turn inwards and study a peculiar feature of timed automata which allows them to enforce behaviors where time distances between events monotonically grow while being bounded by some integer. This feature can be characterized by unbounded counters recording the number of such enforced increases. When we switch from the dense time semantics used for modeling to an implementation with a fixed clock rate (sampled semantics), only behaviors which correspond to a bounded usage of these counters are preserved. We describe operation of these counters as a new type of a counter automaton and prove that one can effectively check whether the counters are used in a bounded way. As a result, it is possible to check for a given timed automaton whether there is an implementation with a fixed sampling rate which preserves all qualitative behaviors.

No description available.

Modern computing platforms strive to support mobile code without putting system security at stake. These platforms can be viewed as open systems, as the mobile code adds new components to the running system. Establishing that such platforms function correctly can  be divided into two steps. First, it is shown that the system functions correctly regardless of the mobile components that join it, provided that they satisfy certain assumptions. These assumptions can, for instance, restrict the behavior of the component to ensure that the security policy of the platform is not violated. Second, the mobile component is checked to satisfy its assumptions, before it is allowed to join the system. This thesis presents algorithmic verification techniques to support this methodology. In the first two parts, we present techniques for the verification of open systems relative to the given component assumptions. In the third part, a technique for the  quick certification of mobile code is presented for the case where a particular type of program rewriting is used as a means of enforcing the component assumptions.In the first part of this study, we present a framework for the verification of open systems based on explicit state space representation. We propose Extended Modal Transition Systems (EMTS) as a suitable structure for representing the state space of open systems when assumptions on components are written in the modal μ-calculus. EMTSs are based on the Modal Transition Systems (MTS) of Larsen and provide a formalism for graphical specification and facilitate a thorough understanding of the system by visualization. In interactive verification, this state space representation enables proof reuse and aids the user guiding the verification process. We present a construction of state space representations from process algebraic open system descriptions based on a maximal model construction for the modal μ-calculus. The construction is sound and complete for systems with a single unknown component and sound for those without dynamic process reation. We also suggest a tableau-based proof system for establishing temporal properties of open systems represented as EMTS. The proof system is sound in general and complete for prime formulae.The problem of open system correctness  also arises in compositional verification, where the problem of showing a global property of a system is reduced to showing local properties of components. In the second part, we extend an existing  compositional verification framework for Java bytecode programs. The framework employs control flow graphs with procedures to model component implementations and open systems for the purpose of checking control-flow properties. We generalize these models to capture exceptional and multi-threaded behavior. The resulting control flow graphs are specifically tailored to support the compositional verification principle; however, they are sufficiently intuitive and standard to be useful on their own. We describe how the models can be extracted from program code and give preliminary experimental results for our implementation of the extraction of control flow graphs with exceptions. We also discuss further tool support and practical applications of the method.In the third part of the thesis, we develop a technique for the certification of safe mobile code, by adapting the proof-carrying code scheme of Necula to the case of security policies expressed as security automata. In particular, we describe how proofs of policy compliance can  be automatically generated for  programs that include a monitor for the desired policy. A monitor is an entity that observes the execution of a program and terminates the program if a violation to the property is about to occur. One way to implement such a monitor is by rewriting the program to make it self-monitoring. Given a property, we characterize self-monitoring of Java bytecode programs for this property by an annotation scheme with annotations in the style of Floyd-Hoare logics. The annotations generated by this scheme can be extended in a straightforward way to form a correctness proof in the sense of axiomatic semantics of programs. The proof generated in this manner essentially establishes that the program satisfies the property because it contains a monitor for it. The annotations that comprise the proofs are simple and efficiently checkable, thus facilitate certification of mobile code on devices with restricted computing power such as mobile phones. / QC 20100628

The Max-Cut problem is a well-known NP-hard problem, for which numerous approximation algorithms have been developed over the years. In this thesis, we examine the special case where the degree of vertices in the graph is bounded. With minor modifications to existing algorithms, we are able to obtain an improved approximation ratio for general bounded-degree graphs. Furthermore we show additional improvements for graphs with at least a constant fraction of odd-degree vertices. We also identify some other possible areas for improvement in the general bounded-degree case. / Max-Cut-problemet är ett välkänt NP-svårt problem, för vilket ett flertal olika approximationsalgoritmer har utvecklats över åren. I det här arbetet undersöks specialfallet då grafens noder har begränsat gradtal. Med mindre förändringar av existerande algoritmer lyckas vi uppnå en förbättrad approximationskvot för generella gradtals-begränsade grafer. Vi visar också ytterligare förbättringar för grafer med minst en konstant andel noder med udda gradtal. Vi identifierar också några andra möjliga områden för förbättring i det allmänna gradtals-begränsade fallet.

Om man ser på de bästa nu kända algoritmerna för att avgöra satisfierbarhet hos logiska formler så är de allra flesta baserade på den så kallade DPLL-metoden utökad med klausulinlärning. De två viktigaste gränssättande faktorerna för sådana algoritmer är hur mycket tid och minne de använder, och att förstå sig på detta är därför en fråga som har stor praktisk betydelse. Inom området beviskomplexitet svarar tids- och minnesåtgång mot längd och minne hos resolutionsbevis för formler i konjunktiv normalform (CNF-formler). En lång rad arbeten har studerat dessa mått och även jämfört dem med bredden av bevis, ett annat mått som visat sig höra nära samman med både längd och minne. Mer formellt är längden hos ett bevis antalet rader, dvs. klausuler, bredden är storleken av den största klausulen, och minnet är maximala antalet klausuler som man behöver komma ihåg samtidigt om man under bevisets gång bara får dra nya slutsatser från klausuler som finns sparade. För längd och bredd har man lyckats visa en rad starka resultat men förståelsen av måttet minne har lämnat mycket i övrigt att önska. Till exempel så är det känt att minnet som behövs för att bevisa en formel är minst lika stort som den nödvändiga bredden, men det har varit en öppen fråga om minne och bredd kan separeras eller om de två måtten mäter "samma sak" i den meningen att de alltid är asymptotiskt lika stora för en formel. Det har också varit okänt om det faktum att det finns ett kort bevis för en formel medför att formeln också kan bevisas i litet minne (motsvarande påstående är sant för längd jämfört med bredd) eller om det tvärtom kan vara så att längd och minne är "helt orelaterade" på så sätt att även korta bevis kan kräva maximal mängd minne. I denna avhandling presenterar vi först ett förenklat bevis av trade-off-resultatet för längd jämfört med minne i (Hertel och Pitassi 2007) och visar hur samma idéer kan användas för att visa ett par andra exponentiella avvägningar i relationerna mellan olika beviskomplexitetsmått för resolution. Sedan visar vi att det finns formler som kan bevisas i linjär längd och konstant bredd men som kräver en mängd minne som växer logaritmiskt i formelstorleken, vilket vi senare förbättrar till kvadratroten av formelstorleken. Dessa resultat separerar således minne och bredd. Genom att använda andra men besläktade idéer besvarar vi därefter frågan om hur minne och längd förhåller sig till varandra genom att separera dem på starkast möjliga sätt. Mer precist visar vi att det finns CNF-formler av storlek O(n) som har resolutionbevis i längd O(n) och bredd O(1) men som kräver minne minst Omega(n/log n). Det gemensamma temat för dessa resultat är att vi studerar formler som beskriver stenläggningsspel, eller pebblingspel, på riktade acykliska grafer. Vi bevisar undre gränser för det minne som behövs för den så kallade pebblingformeln över en graf uttryckt i det svart-vita pebblingpriset för grafen i fråga. Slutligen observerar vi att vår optimala separation av minne och längd i själva verket är ett specialfall av en mer generell sats. Låt F vara en CNF-formel och f:{0,1}^d->{0,1} en boolesk funktion. Ersätt varje variabel x i F med f(x_1, ..., x_d) och skriv om denna nya formel på naturligt sätt som en CNF-formel F[f]. Då gäller, givet att F och f har rätt egenskaper, att F[f] kan bevisas i resolution i väsentligen samma längd och bredd som F, men att den minimala mängd minne som behövs för F[f] är åtminstone lika stor som det minimala antalet variabler som måste förekomma samtidigt i ett bevis för F. / Most state-of-the-art satisfiability algorithms today are variants of the DPLL procedure augmented with clause learning. The two main bottlenecks for such algorithms are the amounts of time and memory used. Thus, understanding time and memory requirements for clause learning algorithms, and how these requirements are related to one another, is a question of considerable practical importance. In the field of proof complexity, these resources correspond to the length and space of resolution proofs for formulas in conjunctive normal form (CNF). There has been a long line of research investigating these proof complexity measures and relating them to the width of proofs, another measure which has turned out to be intimately connected with both length and space. Formally, the length of a resolution proof is the number of lines, i.e., clauses, the width of a proof is the maximal size of any clause in it, and the space is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. While strong results have been established for length and width, our understanding of space has been quite poor. For instance, the space required to prove a formula is known to be at least as large as the needed width, but it has remained open whether space can be separated from width or whether the two measures coincide asymptotically. It has also been unknown whether the fact that a formula is provable in short length implies that it is also provable in small space (which is the case for length versus width), or whether on the contrary these measures are "completely unrelated" in the sense that short proofs can be maximally complex with respect to space. In this thesis, as an easy first observation we present a simplified proof of the recent length-space trade-off result for resolution in (Hertel and Pitassi 2007) and show how our ideas can be used to prove a couple of other exponential trade-offs in resolution. Next, we prove that there are families of CNF formulas that can be proven in linear length and constant width but require space growing logarithmically in the formula size, later improving this exponentially to the square root of the size. These results thus separate space and width. Using a related but different approach, we then resolve the question about the relation between space and length by proving an optimal separation between them. More precisely, we show that there are families of CNF formulas of size O(n) that have resolution proofs of length O(n) and width O(1) but for which any proof requires space Omega(n/log n). All of these results are achieved by studying so-called pebbling formulas defined in terms of pebble games over directed acyclic graphs (DAGs) and proving lower bounds on the space requirements for such formulas in terms of the black-white pebbling price of the underlying DAGs. Finally, we observe that our optimal separation of space and length is in fact a special case of a more general phenomenon. Namely, for any CNF formula F and any Boolean function f:{0,1}^d->{0,1}, replace every variable x in F by f(x_1, ..., x_d) and rewrite this new formula in CNF in the natural way, denoting the resulting formula F[f]. Then if F and f have the right properties, F[f] can be proven in resolution in essentially the same length and width as F but the minimal space needed for F[f] is lower-bounded by the number of variables that have to be mentioned simultaneously in any proof for F. / QC 20100831