Browse Research and Tech Reports - Computer Science by Author "Viswanathan, Mahesh"

  • Prabhakar, Pavithra; Vladimerou, Vladimeros; Viswanathan, Mahesh; Dullerud, Geir E. (2008-01)
    The paper shows the decidability of the reachability problem for planar, monotonic, linear hybrid automata without resets. These automata are a special class of linear hybrid automata with only two variables, whose flows ...

    application/pdf

    application/pdfPDF (193kB)
  • Bhattiprolu, Vijay; Gordon, Spencer; Viswanathan, Mahesh (2017-06-23)
    We prove an analog of Parikh's theorem for weighted context-free grammars over commutative, idempotent semirings, and exhibit a stochastic context-free grammar with behavior that cannot be realized by any stochastic ...

    application/pdf

    application/pdfPDF (299kB)
  • Roohi, Nima; Prabhakar, Pavithra; Viswanathan, Mahesh (2016)

    application/pdf

    application/pdfPDF (660kB)
  • Sobeih, Ahmed A.; Viswanathan, Mahesh; Hou, Jennifer C. (2004-07)
    Existing network simulators perform reasonably well in evaluating the performance of network protocols, but lack the capability of verifying the correctness of network protocols. In this paper, we present our ongoing ...

    application/pdf

    application/pdfPDF (274kB)
  • Vardhan, Abhay; Viswanathan, Mahesh (2005-08)
    We present a new model checking algorithm for verifying computation tree logic (CTL) properties. Our technique is based on using language inference to learn the fixpoints necessary for checking a CTL formula instead of ...

    application/pdf

    application/pdfPDF (232kB)
  • Vardhan, Abhay; Sen, Koushik; Viswanathan, Mahesh; Agha, Gul A. (2004-06)
    We present a novel approach for verifying safety properties of finite state machines communicating over unbounded FIFO channels that is based on applying machine learning techniques. We assume that we are given a model of ...

    application/pdf

    application/pdfPDF (336kB)
  • Kumar, Viraj; Madhusudan, P.; Viswanathan, Mahesh (2006-06)
    Boolean programs with recursion are convenient abstractions of sequential, imperative programs. Recursive state machines (RSM) serve as machine models for Boolean programs and are semantically equivalent to pushdown automata. ...

    application/pdf

    application/pdfPDF (330kB)
  • Sen, Koushik; Viswanathan, Mahesh (2006-01)
    In order to make multithreaded programming manageable, programmers often follow a design principle where they break the problem into tasks which are then solved asynchronously and concurrently on different threads. This ...

    application/pdf

    application/pdfPDF (154kB)
  • Sen, Koushik; Viswanathan, Mahesh; Agha, Gul A. (2006-01)
    We investigate the problem of model checking Interval-valued Discrete-time Markov Chains (IDTMC). IDTMCs are discrete-time finite Markov Chains for which the exact transition probabilities are not known. Instead in IDTMCs, ...

    application/pdf

    application/pdfPDF (246kB)
  • Bauer, Matthew S; Chadha, Rohit; Viswanathan, Mahesh (2017)
    Security protocols that provide privacy and anonymity guarantees are growing increasingly prevalent in the online world. The highly intricate nature of these protocols makes them vulnerable to subtle design flaws. Formal ...

    application/pdf

    application/pdfPDF (558kB)
  • Sen, Koushik; Viswanathan, Mahesh; Agha, Gul A. (2004-12)
    Statistical methods to model check stochastic systems have been, thus far, developed only for a sublogic of continuous stochastic logic (CSL) that does not have steady state operators and unbounded until formulas. In this ...

    application/pdf

    application/pdfPDF (230kB)
  • Chadha, Rohit; Sistla, A. Parsad; Viswanathan, Mahesh (2009-02)
    The continuous run-time monitoring of the behavior of a system is a technique that is used both as a complementary approach to formal verification and testing to ensure reliability, as well as a means to discover emergent ...

    application/pdf

    application/pdfPDF (368kB)
  • Chadha, Rohit; Sistla, A. Parsad; Viswanathan, Mahesh (2009-02)
    The continuous run-time monitoring of the behavior of a system is a technique that is used both as a complementary approach to formal verification and testing to ensure reliability, as well as a means to discover emergent ...

    application/pdf

    application/pdfPDF (368kB)
  • Kini, Dileep; Viswanathan, Mahesh (2017)
    A crucial step in model checking Markov Decision Processes (MDP) is to translate the LTL specification into automata. Efforts have been made in improving deterministic automata construction for LTL but such translations ...

    application/pdf

    application/pdfPDF (452kB)
  • Kini, Dileep; Viswanathan, Mahesh (2015)
    LTL\GU is a fragment of linear temporal logic (LTL), where negations appear only on propositions, and formulas are built using the temporal operators X (next), F (eventually), G (always), and U (until, with the restriction ...

    application/pdf

    application/pdfPDF (368kB)
  • Hendrix, Joe; Ohsaki, Hitoshi; Viswanathan, Mahesh (2006-02)
    In the paper, we introduce a new tree automata framework, called propositional tree automata, capturing the class of tree languages that are closed under an equational theory and Boolean operations. This framework originates ...

    application/pdf

    application/pdfPDF (307kB)
  • Korthikanti, Vijay Anand; Viswanathan, Mahesh; Kwon, YoungMin; Agha, Gul A. (2010)
    We consider Markov Decision Processes (MDPs) as transformers on probability distributions, where with respect to a scheduler that resolves nondeterminism, the MDP can be seen as exhibiting a behavior that is a sequence of ...

    application/pdf

    application/pdfPDF (404kB)
  • Roohi, Nima; Viswanathan, Mahesh (Springer, 2014-06-23)
    Initialized hybrid automata with linear differential inclusions and rectangular constraints are hybrid automata where the invariants, guards, resets, and initial values are given by rectangular constraints, the flows are ...

    application/pdf

    application/pdfPDF (1MB)
  • Chadha, Rohit; Sistla, A. Parsad; Viswanathan, Mahesh (2017-04-18)
    We consider the problem of verifying the security of finitely many sessions of a protocol that tosses coins in addition to standard cryptographic primitives against a Dolev-Yao adversary. Two properties are investigated ...

    application/pdf

    application/pdfPDF (457kB)
  • Sobeih, Ahmed A.; d'Amorim, Marcelo; Viswanathan, Mahesh; Marinov, Darko; Hou, Jennifer C. (2007-08)
    Verification and Validation (V&V) is a critically important phase in the development life cycle of a simulation model. In the context of network simulation, traditional network simulators perform well in using a simulation ...

    application/pdf

    application/pdfPDF (298kB)