uu.seUppsala universitets publikasjoner
Endre søk
Begrens søket
1234567 101 - 150 of 9147
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Treff pr side
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
Merk
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 101. Abdulla, Parosh Aziz
    et al.
    Ben Henda, Noomene
    Mayr, Richard
    Sandberg, Sven
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Stochastic Games with Lossy ChannelsManuskript (Annet vitenskapelig)
  • 102.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    Cederberg, Jonathan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rezine, Ahmed
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Monotonic abstraction for programs with dynamic memory heaps2008Inngår i: Computer Aided Verification / [ed] Gupta A, Malik S, Berlin: Springer-Verlag , 2008, s. 341-354Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach.

  • 103.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    d'Orso, Julien
    Monotonic and downward closed games2008Inngår i: Journal of logic and computation (Print), ISSN 0955-792X, E-ISSN 1465-363X, Vol. 18, nr 1, s. 153-169Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In an earlier work [Abdulla et al. (2000, Information and Computation, 160, 109127)] we presented a general framework for verification of infinite-state transition systems, where the transition relation is monotonic with respect to a well quasi-ordering on the set of states. In this article, we investigate extending the framework from the context of transition systems to that of games with infinite state spaces. We show that monotonic games with safety winning conditions are in general undecidable. In particular, we show this negative results for games which are defined over Petri nets. We identify a subclass of monotonic games, called downward closed games. We provide algorithms for analysing downward closed games subject to safety winning conditions. We apply the algorithm to games played on lossy channel systems. Finally, we show that weak parity games are undecidable for the above classes of games.

  • 104.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    Holík, Lukás
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Composed Bisimulation for Tree Automata2008Inngår i: Implementation and Application of Automata, Springer Berlin/Heidelberg, 2008, s. 212-222Konferansepaper (Fagfellevurdert)
  • 105.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    Holík, Lukás
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Composed bisimulation for tree automata2009Inngår i: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 20, nr 4, s. 685-700Artikkel i tidsskrift (Fagfellevurdert)
  • 106.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bouajjani, Ahmed
    Holík, Lukás
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata2008Inngår i: Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin/Heidelberg, 2008, s. 93-108Konferansepaper (Fagfellevurdert)
  • 107.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Cederberg, Jonathan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kaati, Lisa
    Analyzing the security in the GSM radio network using attack jungles2010Inngår i: Leveraging Applications of Formal Methods, Verification, and Validation: Part I, Berlin: Springer-Verlag , 2010, s. 60-74Konferansepaper (Fagfellevurdert)
  • 108.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Cederberg, Jonathan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Monotonic abstraction for programs with multiply-linked structures2013Inngår i: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 24, nr 2, s. 187-210Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.

  • 109.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Clemente, Lorenzo
    Holík, Lukás
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hong, Chih-Duo
    Mayr, Richard
    Vojnar, Tomás
    Advanced Ramsey-based Büchi automata inclusion testing2011Inngår i: CONCUR 2011 — Concurrency Theory, Springer Berlin/Heidelberg, 2011, s. 187-202Konferansepaper (Fagfellevurdert)
  • 110.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Clemente, Lorenzo
    Holík, Lukás
    Hong, Chih-Duo
    Mayr, Richard
    Vojnar, Tomás
    Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing2010Inngår i: Computer Aided Verification, Berlin: Springer-Verlag , 2010, s. 132-147Konferansepaper (Fagfellevurdert)
  • 111.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Delzanno, Giorgio
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Hong, Chih-Duo
    Rezine, Ahmed
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Constrained monotonic abstraction: A CEGAR for parameterized verification2010Inngår i: CONCUR 2010 – Concurrency Theory, Berlin: Springer-Verlag , 2010, s. 86-101Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In this paper, we develop a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety properties for parameterized systems The main drawback of verification using monotonic abstraction is that it sometimes generates spurious counterexamples Our CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a "Safety Zone" and uses it to refine the abstract transition system of the next iteration We have developed a prototype based on this idea, and our experimentation shows that the approach allows to verify many of the examples that cannot be handled by the original monotonic abstraction approach.

  • 112.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Holik, Lukag
    Vojnar, Tomas
    Mediating for reduction (on minimizing alternating Buchi automata)2014Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 552, s. 26-43Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We propose a new approach for minimizing alternating Buchi automata (ABA). The approach is based on the mediated equivalence on states of an ABA, which is the maximal equivalence contained in the mediated preorder. Two states p and q are related by the mediated preorder if there is a mediator (mediating state) which forward simulates p and backward simulates q. Under further conditions, letting a computation on some word jump from q to p preserves the language as the automaton can anyway already accept the word without jumps by runs through the mediator. We further show how the mediated equivalence can be computed efficiently. Finally, we show that, compared to the standard forward simulation equivalence, the mediated equivalence can yield much larger reductions when applied within the process of complementing Buchi automata where ABA are used as an intermediate model.

  • 113.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Chen, Yu-Fang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Mayr, Richard
    Vojnar, Tomás
    When simulation meets antichains: On checking language inclusion of nondeterministic finite (tree) automata2010Inngår i: Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer-Verlag , 2010, s. 158-174Konferansepaper (Fagfellevurdert)
  • 114.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Clemente, Lorenzo
    Mayr, Richard
    Sandberg, Sven
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Stochastic Parity Games on Lossy Channel Systems2014Inngår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 10, nr 4, artikkel-id 21Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We give an algorithm for solving stochastic parity games with almost-sure winning conditions on lossy channel systems, under the constraint that both players are restricted to finitememory strategies. First, we describe a general framework, where we consider the class of 21/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a finite attractor. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for stochastic game lossy channel systems.

  • 115.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Collomb-Annichini, Aurore
    Bouajjani, Ahmed
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Using Forward Reachability Analysis for Verification of Lossy Channel Systems2004Inngår i: Formal methods in system design, ISSN 0925-9856, E-ISSN 1572-8102, Vol. 25, nr 1, s. 39-65Artikkel i tidsskrift (Fagfellevurdert)
  • 116.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Cyriac, Aiswarya
    Atig, Mohamed Faouzi
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Montali, Marco
    Reachability in database-driven systems with numerical attributes under recency bounding2019Inngår i: Proc. 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, New York: ACM Press, 2019, s. 335-352Konferansepaper (Fagfellevurdert)
  • 117.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Rezine, Ahmed
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Automatic verification of directory-based consistency protocols with graph constraints2011Inngår i: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 22, nr 4, s. 761-782Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings.

  • 118.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Rezine, Ahmed
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Monotonic abstraction in action: Automatic verification of distributed mutex algorithms2008Inngår i: Theoretical Aspects of Computing - ICTAC 2008, Berlin: Springer-Verlag , 2008, s. 50-65Konferansepaper (Fagfellevurdert)
  • 119.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sangnier, Arnaud
    Traverso, Riccardo
    On the verification of timed ad hoc networks2011Inngår i: Formal Modeling and Analysis of Timed Systems: FORMATS 2011, Springer Berlin/Heidelberg, 2011, s. 256-270Konferansepaper (Fagfellevurdert)
  • 120.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Delzanno, Giorgio
    Univ Genoa, I-16126 Genoa, Italy..
    Rezine, Othmane
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Uppsala Univ, Uppsala, Sweden..
    Sangnier, Arnaud
    Univ Paris Diderot, CNRS, LIAFA, Paris, France..
    Traverso, Riccardo
    FBK, Trento, Italy..
    Parameterized verification of time-sensitive models of ad hoc network protocols2016Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 612, s. 1-22Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.

  • 121.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Delzanno, Giorgio
    Van Begin, Laurent
    A classification of the expressive power of well-structured transition systems2011Inngår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 209, nr 3, s. 248-279Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We compare the expressive power of a class of well-structured transition systems that includes relational automata (extensions of), Petri nets, lossy channel systems, constrained multiset rewriting systems, and data nets. For each one of these models we study the class of languages generated by labeled transition systems describing their semantics. We consider here two types of accepting conditions: coverability and reachability of a fixed a priori configuration. In both cases we obtain a strict hierarchy in which constrained multiset rewriting systems is the most expressive model.

  • 122.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Deneux, Johann
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Nilsson, Marcus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Minimization of Non-deterministic Automata with Large Alphabets2006Inngår i: Implementation and Application of Automata, Springer Berlin/Heidelberg, 2006, s. 31-42Konferansepaper (Fagfellevurdert)
  • 123.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. COMPUTER SYSTEMS.
    Deneux, Johann
    Mahata, Pritha
    Nylén, Aletta
    Downward Closed Language Generators2003Rapport (Annet vitenskapelig)
  • 124.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. COMPUTER SYSTEMS.
    Deneux, Johann
    Mahata, Pritha
    Nylén, Aletta
    Forward Reachability Analysis of Timed Petri Nets2003Rapport (Annet vitenskapelig)
  • 125.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Deneux, Johann
    Mahata, Pritha
    Nylén, Aletta
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Using Forward Reachability Analysis for Verification of Timed Petri Nets2007Inngår i: Nordic Journal of Computing, ISSN 1236-6064, Vol. 14, nr 1, s. 1-42Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets by performing symbolic forward reachability analysis. We introduce a formalism, called region generators, for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol, Lynch and Shavit's mutual exclusion protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.

  • 126.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Deneux, Johann
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Ouaknine, Joel
    Quaas, Karin
    Worrell, James
    Universality Analysis for One-Clock Timed Automata2008Inngår i: Fundamenta Informaticae, ISSN 0169-2968, E-ISSN 1875-8681, Vol. 89, nr 4, s. 419-450Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if epsilon-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.

  • 127. Abdulla, Parosh Aziz
    et al.
    d'Orso, Julien
    Jonsson, Bengt
    Nilsson, Marcus
    Saksena, Mayank
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Regular Model Checking for LTL(MSO)2004Inngår i: Proc. 16th Int. Conf. on Computer Aided Verification, LNCSArtikkel i tidsskrift (Fagfellevurdert)
  • 128.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Dwarkadas, Sandhya
    University of Rochester, U.S.A..
    Rezine, Ahmed
    Linköping University.
    Shriraman, Arrvindh
    Simon Fraser University, Canada .
    Yunyun, Zhu
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Verifying safety and liveness for the FlexTM hybrid transactional memory2013Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We consider the verification of safety (strict serializability and abort consistency) and liveness obstruction and livelock freedom) for the hybrid transactional memory framework FlexTM. This framework allows for flexible implementations of transactional memories based on an adaptation of the MESI coherence protocol. FlexTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use of the latest antichain based techniques to handle systems with tens of thousands of states.

  • 129.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holik, Lukas
    Brno University.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rezine, Ahmed
    Linköping University, Department of Computer and Information Science.
    An Integrated Specification and Verification Technique for Highly Concurrent Data Structures2013Inngår i: Tools and Algorithms for the Construction and Analysis of Systems, 2013Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependen- cies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded num- ber of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state au- tomata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verifica- tion, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have imple- mented our method and used it to verify programs, some of which have not been verified by any other automatic method before.

  • 130.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Block me if you can!: Context-sensitive parameterized verification2014Inngår i: Static Analysis: SAS 2014, Springer, 2014, s. 1-17Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski’s mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

  • 131.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Brno Univ Technol, Brno, Czech Republic.
    Parameterized verification through view abstraction2016Inngår i: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 18, nr 5, s. 495-516Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

  • 132.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukáš
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    All for the price of few: (Parameterized verification through view abstraction)2013Inngår i: Verification, Model Checking, and Abstract Interpretation, Springer Berlin/Heidelberg, 2013, s. 476-495Konferansepaper (Fagfellevurdert)
  • 133.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kindahl, Mats
    Model checking race-freeness2008Inngår i: SIGARCH Computer Architecture News, ISSN 0163-5964, E-ISSN 1943-5851, Vol. 36, nr 5, s. 72-79Artikkel i tidsskrift (Fagfellevurdert)
  • 134.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Haziza, Frédéric
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kindahl, Mats
    Model Checking Race-Freeness2008Inngår i: Proc. 1st Swedish Workshop on Multi-Core Computing, 2008, s. 89-96Konferansepaper (Annet vitenskapelig)
  • 135.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Lengál, Ondrej
    Trinh, Cong Quy
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Verification of heap manipulating programs with ordered data by extended forest automata2016Inngår i: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 53, nr 4, s. 357-385Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.

  • 136.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Lengál, Ondrej
    Trinh, Cong Quy
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    Verification of heap manipulating programs with ordered data by extended forest automata2013Inngår i: Automated Technology for Verification and Analysis: ATVA 2013, Springer Berlin/Heidelberg, 2013, s. 224-239Konferansepaper (Fagfellevurdert)
  • 137.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Holík, Lukás
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Vojnar, Tomás
    A uniform (bi-)simulation-based framework for reducing tree automata2009Inngår i: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 251, s. 27-48Artikkel i tidsskrift (Fagfellevurdert)
  • 138.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Högberg, Johanna
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Bisimulation minimization of tree automata2007Inngår i: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 18, nr 4, s. 699-713Artikkel i tidsskrift (Fagfellevurdert)
  • 139.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Iyer, Purushothaman
    Nylen, Aletta
    Unfoldings of Unbounded Petri Nets2000Inngår i: Proc. 12tn Int. Conf. on Computer Aided Verification, Springer Verlag , 2000, s. 495-507Konferansepaper (Fagfellevurdert)
  • 140.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Model checking of systems with many identical timed processes2003Inngår i: Theoretical Computer Science, ISSN 0304-3975, Vol. 290, nr 1, s. 241-264Artikkel i tidsskrift (Fagfellevurdert)
  • 141.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Mahata, Pritha
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    D'Orsi, Julien
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Regular Tree Model Checking2002Inngår i: CAV 2002, 14th Int. Conf. on Computer Aided Verification., 2002, s. 555-568Konferansepaper (Fagfellevurdert)
  • 142.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Nilsson, Marcus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    d'Orso, Julien
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Algorithmic Improvements in Regular Model Checking2003Inngår i: CAV'03, 15th Int. Conf. Computer Aided Verification, 2003, s. 236-248Konferansepaper (Fagfellevurdert)
  • 143.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Nilsson, Marcus
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    D'Orso, Julien
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik. Datorteknik.
    Regular Model Checking made Simple and Efficient2002Inngår i: CONCUR 2002: Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 20-23, 2002, Proceedings, 2002, s. 116-130Konferansepaper (Fagfellevurdert)
  • 144.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Rezine, Ahmed
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Saksena, Mayank
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi.
    Proving Liveness by Backwards Reachability2006Konferansepaper (Fagfellevurdert)
  • 145.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Trinh, Cong Quy
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Fragment abstraction for concurrent shape analysis2018Inngår i: Programming Languages and Systems, Springer, 2018, s. 442-471Konferansepaper (Fagfellevurdert)
  • 146.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kaati, Lisa
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Högberg, Johanna
    Bisimulation Minimization of Tree Automata2006Inngår i: Implementation and Application of Automata, Berlin: Springer-Verlag , 2006, s. 173-185Konferansepaper (Fagfellevurdert)
  • 147.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Krcal, Pavel
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    R-automata2008Inngår i: CONCUR 2008 - Concurrency Theory / [ed] VanBreugel F; Chechik M, Berlin: Springer-Verlag , 2008, s. 67-81Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We introduce R-automata - finite state machines which operate on a finite number of unbounded counters. The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. R-automata can be, for example, used to model systems with resources (modeled by the counters) which are consumed in small parts but which can be replenished at once. We define the language accepted by an R-automaton relative to a natural number D as the set of words allowing a run along which no counter value exceeds D. As the main result, we show decidability of the universality problem, i.e., the problem whether there is a number D such that the corresponding language is universal. We present a proof based on finite monoids and the factorization forest theorem. This theorem was applied for distance automata in [12] - a special case of R-automata with one counter which is never reset. As a second technical contribution, we extend the decidability result to R-automata with Buchi acceptance conditions.

  • 148.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Krcal, Pavel
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sampled semantics of timed automata2010Inngår i: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 6, nr 3, s. 14:1-37Artikkel i tidsskrift (Fagfellevurdert)
  • 149.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Krcal, Pavel
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Sampled universality of timed automata2007Inngår i: Foundations of Software Science and Computational Structures, Proceedings / [ed] Seidl, H, 2007, s. 2-16Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Timed automata can be studied in not only a dense-time setting but also a discrete-time setting. The most common example of discrete-time semantics is the so called sampled semantics (i.e., discrete semantics with a fixed time granularity epsilon). In the real-time setting, the universality problem is known to be undecidable for timed automata. In this work, we study the universality question for the languages accepted by timed automata with sampled semantics. On the negative side, we show that deciding whether for all sampling periods epsilon a timed automaton accepts all timed words in epsilon-sampled semantics is as hard as in the real-time case, i.e., undecidable. On the positive side, we show that checking whether there is a sampling period such that a timed automaton accepts all untimed words in epsilon-sampled semantics is decidable. Our proof uses clock difference relations, developed to characterize the reachability relation for timed automata in connection with sampled semantics.

  • 150.
    Abdulla, Parosh Aziz
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Krcal, Pavel
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Yi, Wang
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Universality of R-automata with value copying2009Inngår i: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 239, s. 131-141Artikkel i tidsskrift (Fagfellevurdert)
1234567 101 - 150 of 9147
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf