Search

k-Hierarchical probabilistic automata (HPA) are probabilistic automata whose states are partitioned into k + 1 levels such that for any state and input symbol, at most one transition goes to a state at the same level, and others go to higher level states. We show that 1-HPA, with acceptance threshold 1/2 (in the finite and infinite word cases) can recognize non-regular languages, and the non-emptiness and non-universality problems for 1-HPA with threshold 1/2 are decidable in EXPTIME and are PSPACE-hard. We present a new sufficient condition when 1-HPA recognize regular languages. We show that the emptiness problem is undecidable for 2-HPAs.

Intelligent Transportation Systems envision a networked environment consisting of vehicles, the infrastructure, and hand-held devices (e.g., smart-phones). The environment will enable numerous safety, mobility, and environmental improvement applications. For example, drivers can be warned of dangers in their local environment or when risking to leave their lane. Furthermore, their visibility range can be expanded by providing highly up-to-date information from areas that are currently invisible. For another example, the road weather—up-to-the-minute visibility, precipitation, and pavement condition information—can be provided at high spatial resolution. Intelligent Transportation efforts are currently being undertaken throughout the world. In addition to the IntelliDrive initiative of the US Department of Transportation, similar efforts exist in Europe, Japan, and China. But these efforts are largely decoupled from, and often incognizant of, the advances in spatio-temporal information management. This paper outlines a spatio-temporal data management language, Transportation Query Language (TranQuyl), which will facilitate the specification of a wide variety of queries of interest to travelers, to transportation agencies, and to industry. Queries in TranQuyl may be processed in either client server mode, or mobile peer-to-peer (P2P) mode, or both. TranQuyl will provide support for the specification of uncertainty either quantitatively or qualitatively as fuzzy queries, for example: “retrieve safety/emergency information around me”. In response, query processing should avoid overloading the traveler with information, and instead present only the most relevant answers to the query.

The paper considers the problem of modeling and analyzing dynamic policies in Trust Management Systems. It presents a general frame work and a specification language FCTL for specifying properties in such systems. Various important security properties such as simple safety, liveness, role containment can all be elegantly specified in this logic. It presents upper and lower bounds for checking classes of formulas specified in this logic for dynamic systems specified in the RT0 Role based Trust Management System.

This paper presents a survey of research work that has been done over the last decade on exploiting symmetry in model checking of concurrent systems. It describes the techniques based on Quotient Structures, Annotated Quotient Structures and Guarded Quotient Structures. It also briefly describes some of the implemented systems.

The problem of complementing Büchi automata arises when developing decision procedures for temporal logics of programs. Unfortunately, previously known constructions for complementing Büchi automata involve a doubly exponential blow-up in the size of the automaton. We present a construction that involves only an exponential blow-up. We use this construction to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove a complexity hierarchy result for quantified propositional temporal logic.