Browse Research and Tech Reports - Computer Science by Author "Agha, Gul A."

  • Kwon, YoungMin; Sundresh, Sameer; Mechitov, Kirill; Agha, Gul A. (2005-06)
    We present an actor platform for wireless sensor networks (WSNs). A typical WSN may consist of hundreds to tens of thousands of tiny nodes embdedded in an environment. Hence, manual reprogramming of nodes for development, ...

    application/pdf

    application/pdfPDF (206Kb)
  • Dinges, Peter; Charalambides, Minas; Agha, Gul A. (2013-04-04)
    Atomic sets are a synchronization mechanism in which the programmer specifies the groups of data that must be accessed as a unit. The compiler can check this specification for consistency, detect deadlocks, and ...

    application/pdf

    application/pdfPDF (471Kb)
  • Koushik, Sen; Agha, Gul A. (2005-10)
    We present an algorithm for automatic testing of distributed programs, such as Unix processes with inter-process communication and Web services. Specifically, we assume that a program consists of a number of asynchronously ...

    application/pdf

    application/pdfPDF (239Kb)
  • Sen, Koushik; Agha, Gul A. (2006-01)
    Testing concurrent programs that accept data inputs is notoriously hard because, beside the large number of possible data inputs, nondeterminism results in an exponentially large number of interleavings of concurrent events. ...

    application/pdf

    application/pdfPDF (277Kb)
  • Sen, Koushik; Marinov, Darko; Agha, Gul A. (2005-06)
    In unit testing, a program is decomposed into units which are collections of functions. A part of unit can be tested by generating inputs for a single entry function. The entry function may contain pointer arguments, in ...

    application/pdf

    application/pdfPDF (232Kb)
  • Sen, Koushik; Rosu, Grigore; Agha, Gul A. (2004-12)
    A generalized predictive analysis technique is proposed for detecting violations of safety properties from apparently successful executions of multithreaded programs. Specifically, we provide an algorithm to monitor ...

    application/pdf

    application/pdfPDF (208Kb)
  • Moinzadeh, Parya; Mechitov, Kirill A.; Shiftehfar, Reza; Abdelzaher, Tarek F.; Agha, Gul A.; Spencer, Billie F., Jr. (2011-09-02)
    Building energy-efficient systems is one of the principal challenges in wireless sensor networks. Dynamic voltage scaling (DVS), a technique to reduce energy consumption by varying the CPU frequency on the fly, has been ...

    application/pdf

    application/pdfPDF (8Mb)
  • Korthikanti, Vijay Anand; Agha, Gul A. (2009-12-17)
    The amount of energy available in some contexts is strictly limited. For example, in mobile computing, available energy is constrained by battery capacity. As multicore processors with a large number of processors, it ...

    application/pdf

    application/pdfPDF (853Kb)
  • Jang, Myeong-Wuk; Ahmed, Amr M.E.; Agha, Gul A. (2004-04)
    An important problem for agents in open multiagent systems is how to find agents that match certain criteria. A number of middle agent services, such as matchmaking and brokering services, have been proposed to address ...

    application/pdf

    application/pdfPDF (6Mb)
  • 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)
  • Moinzadeh, Parya; Mechitov, Kirill A.; Agha, Gul A. (2011-09-02)
    The efficiency of multi-hop communication is a function of the time required for data transfer, or throughput. A key determinant of throughput is the reliability of packet transmission, as measured by the packet reception ...

    application/pdf

    application/pdfPDF (541Kb)
  • Sundresh, Sameer; Kwon, YoungMin; Mechitov, Kirill; Kim, Wooyoung; Agha, Gul A. (2005-03)
    Localization is the process by which sensor networks associate spatial position information with individual sensors' measurements. While manual surveying is sufficient for small-scale prototypes, it is too time-consuming ...

    application/pdf

    application/pdfPDF (111Kb)
  • 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)
  • 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)
  • Agha, Gul A.; Meseguer, Jose; Sen, Koushik (2005-03)
    We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level ...

    application/pdf

    application/pdfPDF (228Kb)
  • 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)
  • Kwon, YoungMin; Mechitov, Kirill; Sundresh, Sameer; Kim, Wooyoung; Agha, Gul A. (2004-06)
    A process which computes the physical locations of nodes in a wireless sensor network is called localization. Self-localization is critical for large-scale sensor networks because manual or assisted localization is often ...

    application/pdf

    application/pdfPDF (797Kb)
  • Dinges, Peter; Agha, Gul A. (2014-09-11)
    Knowing inputs that cover a specific branch or statement in a program is useful for debugging and regression testing. Symbolic backward execution (SBE) is a natural approach to find such targeted inputs. However, SBE ...

    application/pdf

    application/pdfPDF (387Kb)
  • Ahmed, Amr M.E.; Patel, Abhilash; Brown, Tom; Ham, MyungJoo; Jang, Myeong-Wuk; Agha, Gul A. (2004-12)
    In the dynamic distributed task assignment (DDTA) problem, a team of agents is required to accomplish a set of tasks while maximizing the overall team utility. An effective solution to this problem needs to address two ...

    application/pdf

    application/pdfPDF (144Kb)
  • Devaraj, Christo; Nagda, Mehwish; Gupta, Indranil; Agha, Gul A. (2005-04)
    We propose localized and decentralized protocols to construct and maintain an underlay for sensor networks. An underlay lies in between overlay operations (e.g., data indexing, multicast, etc.) and the sensor network itself. ...

    application/pdf

    application/pdfPDF (366Kb)