You searched for +publisher:"Rice University" +contributor:("Chaudhuri, Swarat").
Showing records 1 – 23 of
23 total matches.
No search limiters apply to these results.
Rice University
1.
Bansal, Suguman.
Algorithmic analysis of Regular repeated games.
Degree: MS, Engineering, 2016, Rice University
URL: http://hdl.handle.net/1911/95650 
► The problem on computing rational behaviors in multi-agent systems with selfish agents (Games) has become paramount for the analysis of such systems. {\em Nash equilibria}…
(more)
▼ The problem on computing rational behaviors in multi-agent systems with selfish agents (Games) has become paramount for the analysis of such systems. {\em Nash equilibria} is one of the most central notions of rational behavior. While the problem of computing Nash equilibria in simple games is well understood, the same cannot be said for more complex games. {\em Repeated games} are one such class of games.
In this thesis, we introduce {\em regular repeated games} as a model for repeated games with bounded rationality. In regular repeated games, agent strategies are given by weighted (discounted-sum aggregate), non-deterministic Büchi transducers. We design an algorithm {\ComputeNash} to compute all Nash equilibria in a regular repeated game. The crux of the algorithm lies in determining if a strategy profile is in Nash equilibria or not. For this it is necessary to compare the discounted sum on one infinite execution with that one other executions. Such relational reasoning has not been studies in the literature before. To this end, we introduce the concept of an {\em ω-regular comparators}.
We demonstrate promise of our approach via experimental analysis on case studies: Iterated Prisoner's Dilemma, repeated auctions, and a model of the Bitcoin protocol.
Advisors/Committee Members: Chaudhuri, Swarat (advisor).
Subjects/Keywords: Repeated games; Bounded rationality; Nash equilibira; Nash equilibria computation; Regular repeated games; Automata; Comparators
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Bansal, S. (2016). Algorithmic analysis of Regular repeated games. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/95650
Chicago Manual of Style (16th Edition):
Bansal, Suguman. “Algorithmic analysis of Regular repeated games.” 2016. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/95650.
MLA Handbook (7th Edition):
Bansal, Suguman. “Algorithmic analysis of Regular repeated games.” 2016. Web. 17 Jan 2021.
Vancouver:
Bansal S. Algorithmic analysis of Regular repeated games. [Internet] [Masters thesis]. Rice University; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/95650.
Council of Science Editors:
Bansal S. Algorithmic analysis of Regular repeated games. [Masters Thesis]. Rice University; 2016. Available from: http://hdl.handle.net/1911/95650
Rice University
2.
Lu, Yanxin.
Corpus-Driven Systems for Program Synthesis and Refactoring.
Degree: PhD, Engineering, 2019, Rice University
URL: http://hdl.handle.net/1911/105342
► Programming is a difficult task. Programmers need to deal with small details inside overly complex computer programs. Sometimes it is inevitable for programmers to make…
(more)
▼ Programming is a difficult task. Programmers need to deal with small details inside overly complex computer programs. Sometimes it is inevitable for programmers to make small mistakes. To deal with this problem, software engineering techniques and formal method based techniques have been proposed to help facilitate programming. These techniques include various software engineering methodologies, design patterns, sophisticated testing methods, program repair algorithms, model checking algorithms, and program synthesis methods.
In this thesis, we propose two additional corpus-driven systems for program synthesis and refactoring. We first introduce program splicing, a programming methodology that aims to automate the workflow of copying, pasting, and modifying code available online. Here, the programmer starts by writing a “draft” that mixes unfinished code, natural language comments, and correctness requirements. A program synthesizer that interacts with a large, searchable database of program snippets is used to automatically complete the draft into a program that meets the requirements. Our evaluation uses the system in a suite of everyday programming tasks, and includes a comparison with a state-of-the-art competing approach as well as a user study. The results point to the broad scope and scalability of program splicing and indicate that the approach can significantly boost programmer productivity. Next, we propose an algorithm that automates the process of API refactoring, where the goal is to rewrite an API call sequence into another sequence that only uses the API calls defined in the target library without modifying the functionality. We solve the problem of API refactoring by combining the techniques of API translation and API sequence synthesis. We evaluated our algorithm on a diverse set of benchmark problems, and our algorithm can refactor API sequences with high accuracy. In addition, we conducted a user study which indicates that our algorithm can help human developers with API refactoring.
Advisors/Committee Members: Chaudhuri, Swarat (advisor).
Subjects/Keywords: Program Synthesis; Big Data; Machine Learning
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Lu, Y. (2019). Corpus-Driven Systems for Program Synthesis and Refactoring. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/105342
Chicago Manual of Style (16th Edition):
Lu, Yanxin. “Corpus-Driven Systems for Program Synthesis and Refactoring.” 2019. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/105342.
MLA Handbook (7th Edition):
Lu, Yanxin. “Corpus-Driven Systems for Program Synthesis and Refactoring.” 2019. Web. 17 Jan 2021.
Vancouver:
Lu Y. Corpus-Driven Systems for Program Synthesis and Refactoring. [Internet] [Doctoral dissertation]. Rice University; 2019. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/105342.
Council of Science Editors:
Lu Y. Corpus-Driven Systems for Program Synthesis and Refactoring. [Doctoral Dissertation]. Rice University; 2019. Available from: http://hdl.handle.net/1911/105342
Rice University
3.
Rahbar, Afsaneh.
Learning Program Invariants from Proof Corpora.
Degree: MS, Engineering, 2018, Rice University
URL: http://hdl.handle.net/1911/105626
► In program verification, loop invariants are of particular interest. Indeed, writing a correct and useful invariant is as challenging as verifying the program itself. Current…
(more)
▼ In program verification, loop invariants are of particular interest. Indeed, writing
a correct and useful invariant is as challenging as verifying the program itself.
Current approaches to solving the problem of automatically generating invariants either
generate invariants by analyzing the program or using machine learning to learn
from program input and output examples, counterexamples, and so on. Each of these
approaches works on particular type of programs and specific data structures. In
this thesis, we describe the technique we have developed for generating these loop
invariants automatically. We introduce a more general learning technique that learns
from a database of annotated verified programs. Our new data-driven approach uses
the existing proofs to learn proof templates, or as we call them proof blocks. In
our method, the algorithm iterates over all possible proof block formulas by using
logical connectors until it finds an appropriate invariant formula. We evaluated our
approach on benchmarks and demonstrated the potential of our technique in verification
of programs. Using the approach of learning from verified annotated programs
makes invariant generation easier and reduces the burden on the verification engineer.
Advisors/Committee Members: Chaudhuri, Swarat (advisor).
Subjects/Keywords: Invariants; Proof Synthesis; Program verification; Hoare logic
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Rahbar, A. (2018). Learning Program Invariants from Proof Corpora. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/105626
Chicago Manual of Style (16th Edition):
Rahbar, Afsaneh. “Learning Program Invariants from Proof Corpora.” 2018. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/105626.
MLA Handbook (7th Edition):
Rahbar, Afsaneh. “Learning Program Invariants from Proof Corpora.” 2018. Web. 17 Jan 2021.
Vancouver:
Rahbar A. Learning Program Invariants from Proof Corpora. [Internet] [Masters thesis]. Rice University; 2018. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/105626.
Council of Science Editors:
Rahbar A. Learning Program Invariants from Proof Corpora. [Masters Thesis]. Rice University; 2018. Available from: http://hdl.handle.net/1911/105626
Rice University
4.
Feser, Jack Killian.
Inductive Program Synthesis from Input-Output Examples.
Degree: MS, Engineering, 2016, Rice University
URL: http://hdl.handle.net/1911/96260
► We present a method for example-guided synthesis of higher-order functional pro- grams. Given a set of input-output examples, our method synthesizes a program in a…
(more)
▼ We present a method for example-guided synthesis of higher-order functional pro- grams. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples.
Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input-output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs.
We have implemented our method in a tool called λ2, and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of λ2. A highlight is the synthesis of a program believed to be the world’s earliest functional pearl.
Advisors/Committee Members: Chaudhuri, Swarat (advisor).
Subjects/Keywords: program synthesis; programming by example; higher-order programs; recursive data structures
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Feser, J. K. (2016). Inductive Program Synthesis from Input-Output Examples. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/96260
Chicago Manual of Style (16th Edition):
Feser, Jack Killian. “Inductive Program Synthesis from Input-Output Examples.” 2016. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/96260.
MLA Handbook (7th Edition):
Feser, Jack Killian. “Inductive Program Synthesis from Input-Output Examples.” 2016. Web. 17 Jan 2021.
Vancouver:
Feser JK. Inductive Program Synthesis from Input-Output Examples. [Internet] [Masters thesis]. Rice University; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/96260.
Council of Science Editors:
Feser JK. Inductive Program Synthesis from Input-Output Examples. [Masters Thesis]. Rice University; 2016. Available from: http://hdl.handle.net/1911/96260
Rice University
5.
Shah, Ameesh.
Differentiable Program Learning with an Admissible Neural Heuristic.
Degree: MS, Engineering, 2020, Rice University
URL: http://hdl.handle.net/1911/109184
► We study the problem of learning differentiable functions expressed as programs in a domain-specific language. Such programmatic models can offer benefits such as composability and…
(more)
▼ We study the problem of learning differentiable functions expressed as programs in a domain-specific language. Such programmatic models can offer benefits such as composability and interpretability; however, learning them requires optimizing over a combinatorial space of program “architectures”. We frame this optimization problem
as a search in a weighted graph whose paths encode top-down derivations of program syntax. Our key innovation is to view various classes of neural networks as continuous relaxations over the space of programs, which can then be used to complete any partial program. This relaxed program is differentiable and can be trained end-to-end, and the resulting training loss is an approximately admissible heuristic that can guide the combinatorial search. We instantiate our approach on top of the A* algorithm and an iteratively deepened branch-and-bound search, and use these algorithms to learn programmatic classifiers in three sequence classification tasks. Our experiments show that the algorithms outperform state-of-the-art methods for program learning, and that they discover programmatic classifiers that yield natural interpretations and achieve competitive accuracy.
Advisors/Committee Members: Jermaine, Chris (advisor), Chaudhuri, Swarat (advisor).
Subjects/Keywords: Machine Learning; Program Synthesis; Functional Programming; Differentiable Progamming
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Shah, A. (2020). Differentiable Program Learning with an Admissible Neural Heuristic. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/109184
Chicago Manual of Style (16th Edition):
Shah, Ameesh. “Differentiable Program Learning with an Admissible Neural Heuristic.” 2020. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/109184.
MLA Handbook (7th Edition):
Shah, Ameesh. “Differentiable Program Learning with an Admissible Neural Heuristic.” 2020. Web. 17 Jan 2021.
Vancouver:
Shah A. Differentiable Program Learning with an Admissible Neural Heuristic. [Internet] [Masters thesis]. Rice University; 2020. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/109184.
Council of Science Editors:
Shah A. Differentiable Program Learning with an Admissible Neural Heuristic. [Masters Thesis]. Rice University; 2020. Available from: http://hdl.handle.net/1911/109184
Rice University
6.
Wang, Yue.
Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.
Degree: PhD, Engineering, 2018, Rice University
URL: http://hdl.handle.net/1911/106178
► Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for…
(more)
▼ Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for building these autonomous robots. Partially Observable Markov Decision Processes (POMDPs) provide a standard approach to model many robot applications under uncertainty. A key algorithmic problem for POMDPs is the synthesis of policies that specify the actions to take contingent on all possible events. Policy synthesis for POMDPs with two kinds of objectives is considered in this thesis: (1) boolean objectives for a correctness guarantee of accomplishing tasks and (2) quantitative objectives for optimal behaviors. For boolean objectives, this thesis focuses on a common safe-reachability objective: with a probability above a threshold, a goal state is eventually reached while keeping the probability of visiting unsafe states below a different threshold. Previous results have shown that policy synthesis for POMDPs over infinite horizon is generally undecidable. For decidability, this thesis focuses on POMDPs over a bounded horizon. Solving POMDPs requires reasoning over a vast space of beliefs (probability distributions). To address this, this thesis introduces the notion of a goal-constrained belief space that only contains beliefs reachable under desired executions that can achieve the safe-reachability objectives. Based on this notion, this thesis presents an offline approach that constructs policies over the goal-constrained belief space instead of the entire belief space. Simulation experiments show that this offline approach can scale to large belief spaces by focusing on the goal-constrained belief space. A full policy is generally costly to compute. To improve efficiency, this thesis presents an online approach that interleaves the computation of partial policies and execution. A partial policy is parameterized by a replanning probability and only contain a sampled subset of all possible events. This online approach allows users to specify an appropriate bound on the replanning probability to balance efficiency and correctness. Finally, this thesis presents an approximate policy synthesis approach that combines the safe-reachability objectives with the quantitative objectives. The results demonstrate that the constructed policies not only achieve the safe-reachability objective but also are of high quality concerning the quantitative objective.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Kavraki, Lydia E (advisor).
Subjects/Keywords: Robotics; Formal Methods; Planning under Uncertainty; POMDPs; Policy
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Wang, Y. (2018). Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/106178
Chicago Manual of Style (16th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/106178.
MLA Handbook (7th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Web. 17 Jan 2021.
Vancouver:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Internet] [Doctoral dissertation]. Rice University; 2018. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/106178.
Council of Science Editors:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Doctoral Dissertation]. Rice University; 2018. Available from: http://hdl.handle.net/1911/106178
Rice University
7.
Wang, Yue.
Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.
Degree: PhD, Computer Science, 2018, Rice University
URL: http://hdl.handle.net/1911/108015
► Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for…
(more)
▼ Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for building these autonomous robots. Partially Observable Markov Decision Processes (POMDPs) provide a standard approach to model many robot applications under uncertainty. A key algorithmic problem for POMDPs is the synthesis of policies that specify the actions to take contingent on all possible events. Policy synthesis for POMDPs with two kinds of objectives is considered in this thesis: (1) boolean objectives for a correctness guarantee of accomplishing tasks and (2) quantitative objectives for optimal behaviors. For boolean objectives, this thesis focuses on a common safe-reachability objective: with a probability above a threshold, a goal state is eventually reached while keeping the probability of visiting unsafe states below a different threshold. Previous results have shown that policy synthesis for POMDPs over infinite horizon is generally undecidable. For decidability, this thesis focuses on POMDPs over a bounded horizon. Solving POMDPs requires reasoning over a vast space of beliefs (probability distributions). To address this, this thesis introduces the notion of a goal-constrained belief space that only contains beliefs reachable under desired executions that can achieve the safe-reachability objectives. Based on this notion, this thesis presents an offline approach that constructs policies over the goal-constrained belief space instead of the entire belief space. Simulation experiments show that this offline approach can scale to large belief spaces by focusing on the goal-constrained belief space. A full policy is generally costly to compute. To improve efficiency, this thesis presents an online approach that interleaves the computation of partial policies and execution. A partial policy is parameterized by a replanning probability and only contain a sampled subset of all possible events. This online approach allows users to specify an appropriate bound on the replanning probability to balance efficiency and correctness. Finally, this thesis presents an approximate policy synthesis approach that combines the safe-reachability objectives with the quantitative objectives. The results demonstrate that the constructed policies not only achieve the safe-reachability objective but also are of high quality concerning the quantitative objective.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Kavraki, Lydia E (advisor).
Subjects/Keywords: Robotics; Formal Methods; Planning under Uncertainty; POMDPs; Policy
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Wang, Y. (2018). Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/108015
Chicago Manual of Style (16th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/108015.
MLA Handbook (7th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Web. 17 Jan 2021.
Vancouver:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Internet] [Doctoral dissertation]. Rice University; 2018. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/108015.
Council of Science Editors:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Doctoral Dissertation]. Rice University; 2018. Available from: http://hdl.handle.net/1911/108015
Rice University
8.
Wang, Yue.
Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.
Degree: PhD, Computer Science, 2018, Rice University
URL: http://hdl.handle.net/1911/105879
► Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for…
(more)
▼ Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for building these autonomous robots. Partially Observable Markov Decision Processes (POMDPs) provide a standard approach to model many robot applications under uncertainty. A key algorithmic problem for POMDPs is the synthesis of policies that specify the actions to take contingent on all possible events. Policy synthesis for POMDPs with two kinds of objectives is considered in this thesis: (1) boolean objectives for a correctness guarantee of accomplishing tasks and (2) quantitative objectives for optimal behaviors. For boolean objectives, this thesis focuses on a common safe-reachability objective: with a probability above a threshold, a goal state is eventually reached while keeping the probability of visiting unsafe states below a different threshold. Previous results have shown that policy synthesis for POMDPs over infinite horizon is generally undecidable. For decidability, this thesis focuses on POMDPs over a bounded horizon. Solving POMDPs requires reasoning over a vast space of beliefs (probability distributions). To address this, this thesis introduces the notion of a goal-constrained belief space that only contains beliefs reachable under desired executions that can achieve the safe-reachability objectives. Based on this notion, this thesis presents an offline approach that constructs policies over the goal-constrained belief space instead of the entire belief space. Simulation experiments show that this offline approach can scale to large belief spaces by focusing on the goal-constrained belief space. A full policy is generally costly to compute. To improve efficiency, this thesis presents an online approach that interleaves the computation of partial policies and execution. A partial policy is parameterized by a replanning probability and only contain a sampled subset of all possible events. This online approach allows users to specify an appropriate bound on the replanning probability to balance efficiency and correctness. Finally, this thesis presents an approximate policy synthesis approach that combines the safe-reachability objectives with the quantitative objectives. The results demonstrate that the constructed policies not only achieve the safe-reachability objective but also are of high quality concerning the quantitative objective.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Kavraki, Lydia E (advisor).
Subjects/Keywords: Robotics; Formal Methods; Planning under Uncertainty; POMDPs; Policy
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Wang, Y. (2018). Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/105879
Chicago Manual of Style (16th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/105879.
MLA Handbook (7th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Web. 17 Jan 2021.
Vancouver:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Internet] [Doctoral dissertation]. Rice University; 2018. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/105879.
Council of Science Editors:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Doctoral Dissertation]. Rice University; 2018. Available from: http://hdl.handle.net/1911/105879
Rice University
9.
Wang, Yue.
Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.
Degree: PhD, Engineering, 2018, Rice University
URL: http://hdl.handle.net/1911/105878
► Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for…
(more)
▼ Robots are being deployed for many real-world applications like autonomous driving, disaster rescue, and personal assistance. Effectively planning robust executions under uncertainty is critical for building these autonomous robots. Partially Observable Markov Decision Processes (POMDPs) provide a standard approach to model many robot applications under uncertainty. A key algorithmic problem for POMDPs is the synthesis of policies that specify the actions to take contingent on all possible events. Policy synthesis for POMDPs with two kinds of objectives is considered in this thesis: (1) boolean objectives for a correctness guarantee of accomplishing tasks and (2) quantitative objectives for optimal behaviors. For boolean objectives, this thesis focuses on a common safe-reachability objective: with a probability above a threshold, a goal state is eventually reached while keeping the probability of visiting unsafe states below a different threshold. Previous results have shown that policy synthesis for POMDPs over infinite horizon is generally undecidable. For decidability, this thesis focuses on POMDPs over a bounded horizon. Solving POMDPs requires reasoning over a vast space of beliefs (probability distributions). To address this, this thesis introduces the notion of a goal-constrained belief space that only contains beliefs reachable under desired executions that can achieve the safe-reachability objectives. Based on this notion, this thesis presents an offline approach that constructs policies over the goal-constrained belief space instead of the entire belief space. Simulation experiments show that this offline approach can scale to large belief spaces by focusing on the goal-constrained belief space. A full policy is generally costly to compute. To improve efficiency, this thesis presents an online approach that interleaves the computation of partial policies and execution. A partial policy is parameterized by a replanning probability and only contain a sampled subset of all possible events. This online approach allows users to specify an appropriate bound on the replanning probability to balance efficiency and correctness. Finally, this thesis presents an approximate policy synthesis approach that combines the safe-reachability objectives with the quantitative objectives. The results demonstrate that the constructed policies not only achieve the safe-reachability objective but also are of high quality concerning the quantitative objective.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Kavraki, Lydia E. (committee member).
Subjects/Keywords: Robotics; Formal Methods; Planning under Uncertainty; POMDPs; Policy
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Wang, Y. (2018). Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/105878
Chicago Manual of Style (16th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/105878.
MLA Handbook (7th Edition):
Wang, Yue. “Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives.” 2018. Web. 17 Jan 2021.
Vancouver:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Internet] [Doctoral dissertation]. Rice University; 2018. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/105878.
Council of Science Editors:
Wang Y. Bounded Policy Synthesis for POMDPs with Safe-Reachability and Quantitative Objectives. [Doctoral Dissertation]. Rice University; 2018. Available from: http://hdl.handle.net/1911/105878
Rice University
10.
Lu, Yanxin.
Improving Peer Evaluation Quality in Massive Open Online Courses.
Degree: MS, Engineering, 2015, Rice University
URL: http://hdl.handle.net/1911/88103
► As several online course providers such as Coursera, Udacity and edX emerged in 2012, Massive Open Online Courses (MOOCs) gained much attention across the globe.…
(more)
▼ As several online course providers such as Coursera, Udacity and edX emerged in 2012, Massive Open Online Courses (MOOCs) gained much attention across the globe. While MOOCs provide learning opportunities for many people, several challenges exist in the context of MOOC and one of those is how to ensure the quality of peer grading. Interactive Programming in Python course (IPP) that
Rice has offered for a number of years on Coursera has suffered from the problem of low-quality peer evaluations. In this thesis, we propose our solution to improve the quality of peer evaluations by motivating peer graders. Specifically, we want to answer the question: when a student knows that his or her own peer grading efforts are being examined and they are able to grade other peer evaluations, do those tend to motivate the student to do a better job when grading assignments? We implemented a web application where students can grade peer evaluations and we also conduct a series of controlled experiments. Finally, we find a strong effect on peer evaluation quality simply because students know that they are going to be studied using a software that is supposed to help with peer grading. In addition, we find strong evidence that by grading peer evaluations students tend to give better peer evaluations. However, the strongest effect seems to be obtained via the act of grading others’ evaluations, and not from the knowledge that one’s own peer evaluation will be examined.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Warren, Joe (committee member), Jermaine, Chris (committee member).
Subjects/Keywords: MOOC; Peer Evaluation; Education
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Lu, Y. (2015). Improving Peer Evaluation Quality in Massive Open Online Courses. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/88103
Chicago Manual of Style (16th Edition):
Lu, Yanxin. “Improving Peer Evaluation Quality in Massive Open Online Courses.” 2015. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88103.
MLA Handbook (7th Edition):
Lu, Yanxin. “Improving Peer Evaluation Quality in Massive Open Online Courses.” 2015. Web. 17 Jan 2021.
Vancouver:
Lu Y. Improving Peer Evaluation Quality in Massive Open Online Courses. [Internet] [Masters thesis]. Rice University; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88103.
Council of Science Editors:
Lu Y. Improving Peer Evaluation Quality in Massive Open Online Courses. [Masters Thesis]. Rice University; 2015. Available from: http://hdl.handle.net/1911/88103
Rice University
11.
Imam, Shams Mahmood.
Cooperative Execution of Parallel Tasks with Synchronization Constraints.
Degree: PhD, Engineering, 2015, Rice University
URL: http://hdl.handle.net/1911/88129
► The topic of this thesis is the effective execution of parallel applications on emerging multicore and manycore systems in the presence of modern synchronization and…
(more)
▼ The topic of this thesis is the effective execution of parallel applications on emerging multicore and manycore systems in the presence of modern synchronization and coordination constraints. Synchronization and coordination can contribute significant productivity and performance overheads to the development and execution of parallel programs. Higher-level programming models, such as the Task Parallel Model and Actor Model, provide abstractions that can be used to simplify writing parallel programs, in contrast to lower-level programming models that directly expose locks, threads and processes. However, these higher-level models often lack efficient support for general synchronization patterns that are necessary for a wide range of applications. Many modern synchronization and coordination constructs in parallel programs can incur significant performance overheads on current runtime systems, or significant productivity overheads when the programmer is forced to complicate their code to mitigate these performance overheads. We believe that a cooperation between the programmer and the runtime system is necessary to reduce the parallel overhead and to execute the available parallelism efficiently in the presence of synchronization constraints. In a cooperative approach, an executing entity yields control to other entities at well-defined points during its execution. This thesis shows that the use of cooperative techniques is critical to performance and scalability of certain parallel programming models, especially in the presence of modern synchronization and coordination constraints such as asynchronous tasks, futures, phasers, data-driven tasks, and actors. In particular, we focus on cooperative extensions and runtimes for the async-finish Task Parallel Model and the Actor Model in this thesis. Our work shows that cooperative techniques simplify programmability and deliver significant performance improvements by reducing the overhead in modern parallel programming models.
Advisors/Committee Members: Sarkar, Vivek (advisor), Mellor-Crummey, John (committee member), Chaudhuri, Swarat (committee member), Zhong, Lin (committee member).
Subjects/Keywords: Cooperative Techniques; Cooperative Runtime; Synchronization Constraints; Eureka Programming Model; Selector Model; Task Parallel Model; Actor Model; Habanero Java
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Imam, S. M. (2015). Cooperative Execution of Parallel Tasks with Synchronization Constraints. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/88129
Chicago Manual of Style (16th Edition):
Imam, Shams Mahmood. “Cooperative Execution of Parallel Tasks with Synchronization Constraints.” 2015. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88129.
MLA Handbook (7th Edition):
Imam, Shams Mahmood. “Cooperative Execution of Parallel Tasks with Synchronization Constraints.” 2015. Web. 17 Jan 2021.
Vancouver:
Imam SM. Cooperative Execution of Parallel Tasks with Synchronization Constraints. [Internet] [Doctoral dissertation]. Rice University; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88129.
Council of Science Editors:
Imam SM. Cooperative Execution of Parallel Tasks with Synchronization Constraints. [Doctoral Dissertation]. Rice University; 2015. Available from: http://hdl.handle.net/1911/88129
Rice University
12.
Wang, Yue.
A Constraint-Based Approach to Reactive Task and Motion Planning.
Degree: MS, Engineering, 2016, Rice University
URL: http://hdl.handle.net/1911/88419
► This thesis presents a novel and scalable approach for Reactive Task and Motion Planning. We consider changing environments with uncontrollable agents, where the robot needs…
(more)
▼ This thesis presents a novel and scalable approach for Reactive Task and Motion Planning. We consider changing environments with uncontrollable agents, where the robot needs a policy to respond correctly in the infinite interaction with the environment. Our approach operates on task and motion domains that combine actions over discrete states with continuous, collision-free paths. We synthesize a policy by iteratively verifying and searching for a policy candidate. For efficient verification, we employ Satisfiability Modulo Theories (SMT) solvers using a new extension of proof rules for Temporal Property Verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures. Furthermore, the SMT solver enables quantitative specifications such as energy limits. We benchmark our policy synthesizer in a mobile manipulation domain, showing that our approach offers better scalability compared to a state-of-the-art robotic synthesis tool in the tested benchmarks and demonstrating order-of-magnitude speedup from our heuristics.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Kavraki, Lydia E (committee member), Vardi, Moshe Y (committee member).
Subjects/Keywords: Constraint-based approaches; Reactive synthesis; Syntax-guided synthesis; Mobile manipulation
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Wang, Y. (2016). A Constraint-Based Approach to Reactive Task and Motion Planning. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/88419
Chicago Manual of Style (16th Edition):
Wang, Yue. “A Constraint-Based Approach to Reactive Task and Motion Planning.” 2016. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88419.
MLA Handbook (7th Edition):
Wang, Yue. “A Constraint-Based Approach to Reactive Task and Motion Planning.” 2016. Web. 17 Jan 2021.
Vancouver:
Wang Y. A Constraint-Based Approach to Reactive Task and Motion Planning. [Internet] [Masters thesis]. Rice University; 2016. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88419.
Council of Science Editors:
Wang Y. A Constraint-Based Approach to Reactive Task and Motion Planning. [Masters Thesis]. Rice University; 2016. Available from: http://hdl.handle.net/1911/88419
Rice University
13.
Vrvilo, Nick.
Implementing Asynchronous Checkpoint/Restart for the Concurrent Collections Model.
Degree: MS, Engineering, 2014, Rice University
URL: http://hdl.handle.net/1911/88191
► It has been claimed that what simplifies parallelism can also simplify resilience. Based on that assertion, we present the Concurrent Collections programming model (CnC) as…
(more)
▼ It has been claimed that what simplifies parallelism can also simplify resilience. Based on that assertion, we present the Concurrent Collections programming model (CnC) as an ideal target for a simple yet powerful resilience system for parallel computations. Specifically, we claim that the same attributes that simplify reasoning about parallel applications written in CnC will similarly simplify the implementation of a checkpoint/restart system within the CnC runtime. We define these properties of CnC in the context of a model built in K. To demonstrate how these simplifying properties of CnC help to simplify resilience, we have implemented a simple checkpoint/restart system within Rice’s Habanero C implementation of the CnC runtime. We show how the CnC runtime can fully encapsulate the checkpointing and restarting processes, allowing application programmers to gain all the benefits of resilience without any added effort beyond implementing the application in CnC, while avoiding the synchronization overheads present in traditional techniques.
Advisors/Committee Members: Sarkar, Vivek (advisor), Mellor-Crummey, John (committee member), Chaudhuri, Swarat (committee member).
Subjects/Keywords: Concurrent Collections; Resilience; Checkpoint/Restart
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Vrvilo, N. (2014). Implementing Asynchronous Checkpoint/Restart for the Concurrent Collections Model. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/88191
Chicago Manual of Style (16th Edition):
Vrvilo, Nick. “Implementing Asynchronous Checkpoint/Restart for the Concurrent Collections Model.” 2014. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88191.
MLA Handbook (7th Edition):
Vrvilo, Nick. “Implementing Asynchronous Checkpoint/Restart for the Concurrent Collections Model.” 2014. Web. 17 Jan 2021.
Vancouver:
Vrvilo N. Implementing Asynchronous Checkpoint/Restart for the Concurrent Collections Model. [Internet] [Masters thesis]. Rice University; 2014. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88191.
Council of Science Editors:
Vrvilo N. Implementing Asynchronous Checkpoint/Restart for the Concurrent Collections Model. [Masters Thesis]. Rice University; 2014. Available from: http://hdl.handle.net/1911/88191
Rice University
14.
He, Keliang.
Robot Manipulation Planning Under Linear Temporal Logic Specifications.
Degree: MS, Engineering, 2015, Rice University
URL: http://hdl.handle.net/1911/88079
► Automated planning for manipulation tasks is highly desirable, for it enables robot manipulators to be used by none robotics experts. This thesis presents one approach…
(more)
▼ Automated planning for manipulation tasks is highly desirable, for it enables robot manipulators to be used by none robotics experts. This thesis presents one approach to solving manipulation planning for tasks expressed in linear temporal logic (ltl). This approach is based on the synergistic framework, which provides probabilistic completeness guarantees. Even though the synergistic framework has shown to work well for planning for ltl tasks in the navigation domain, it lacked an abstraction that can capture the high dimensionality of manipulation. This thesis enables manipulation planning using the synergistic framework by introducing a manipulation abstraction and modifying the interaction between task and motion planning in the framework. The modified framework is shown to be effectively in case studies in both simulation and physical systems. The case studies also show that the synergistic framework plans for manipulation problems more effective using the manipulation abstraction in comparison with a naive abstraction.
Advisors/Committee Members: Kavraki, Lydia E (advisor), Vardi, Moshe Y (committee member), Chaudhuri, Swarat (committee member).
Subjects/Keywords: Robot Manipulation; Integrated Task and Motion Planning
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
He, K. (2015). Robot Manipulation Planning Under Linear Temporal Logic Specifications. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/88079
Chicago Manual of Style (16th Edition):
He, Keliang. “Robot Manipulation Planning Under Linear Temporal Logic Specifications.” 2015. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88079.
MLA Handbook (7th Edition):
He, Keliang. “Robot Manipulation Planning Under Linear Temporal Logic Specifications.” 2015. Web. 17 Jan 2021.
Vancouver:
He K. Robot Manipulation Planning Under Linear Temporal Logic Specifications. [Internet] [Masters thesis]. Rice University; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88079.
Council of Science Editors:
He K. Robot Manipulation Planning Under Linear Temporal Logic Specifications. [Masters Thesis]. Rice University; 2015. Available from: http://hdl.handle.net/1911/88079
Rice University
15.
Zhou, Yu.
Swarm Robotics: Measurement and Sorting.
Degree: MS, Engineering, 2015, Rice University
URL: http://hdl.handle.net/1911/88413
► To measure is an important ability for robots to sense the environment and nearby robots. Although camera, laser, and ultrasonic provide very accurate measurements, they…
(more)
▼ To measure is an important ability for robots to sense the environment and nearby robots. Although camera, laser, and ultrasonic provide very accurate measurements, they are expensive and not scalable for large swarm of low-cost robots. The r-one robot designed at
Rice University is equipped with infrared transmitters and receivers, which are designed for remote control and are very inexpensive in mass production. They are a good solution for short-range communication, since the signal attenuates at about 1 to 2 meters with appropriate voltage. This work describes my results in using them to measure bearing, orientation, and distance between nearby robots. However, infrared receivers are not designed for this kind of use, so I present a variable transmit power approach to allow useful and efficient local geometry measurements.
With the ability to measure bearing and distance, I am able to solve the problem of sorting a group of n robots in a two-dimensional space. I want to organize robots into a sorted and equally-spaced path between the robots with lowest and highest label, while maintaining a connected communication network throughout the process. I begin with a straightforward geometry-based version of sorting algorithm, and point out there are many difficulties when communication range becomes limited.
Then I describe a topology-based distributed algorithm for this task. I introduce operations to break the symmetry between minimum and maximum, in order to keep time, travel distance, and communication costs low without using central control. I run a set of algorithms (leader election, tree formation, path formation, path modification, and geometric straightening) in parallel. I show that my overall approach is safe, correct, and efficient. It is robust to population changes, network connectivity changes, and sensor errors. I validate my theoretical results with simulation results. My algorithm implementation uses communication messages of fixed size and constant memory on each robot, and is a practical solution for large populations of low-cost robots.
Advisors/Committee Members: McLurkin, James D. (advisor), Kavraki, Lydia E (committee member), Chaudhuri, Swarat (committee member).
Subjects/Keywords: Swarm Robotics; Physical Sorting; Distributed Algorithms
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Zhou, Y. (2015). Swarm Robotics: Measurement and Sorting. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/88413
Chicago Manual of Style (16th Edition):
Zhou, Yu. “Swarm Robotics: Measurement and Sorting.” 2015. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88413.
MLA Handbook (7th Edition):
Zhou, Yu. “Swarm Robotics: Measurement and Sorting.” 2015. Web. 17 Jan 2021.
Vancouver:
Zhou Y. Swarm Robotics: Measurement and Sorting. [Internet] [Masters thesis]. Rice University; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88413.
Council of Science Editors:
Zhou Y. Swarm Robotics: Measurement and Sorting. [Masters Thesis]. Rice University; 2015. Available from: http://hdl.handle.net/1911/88413
Rice University
16.
Fang, Ye.
computer-aided mechanism design.
Degree: MS, Engineering, 2015, Rice University
URL: http://hdl.handle.net/1911/87798
► Algorithmic mechanism design, as practised today, is a manual process; however, manual design and reasoning do not scale well with the complexity of design tasks.…
(more)
▼ Algorithmic mechanism design, as practised today, is a manual process; however, manual design and reasoning do not scale well with the complexity of design tasks. In this thesis, we study computer-aided mechanism design as an alternative to manual construction and analysis of mechanisms. In our approach, a mechanism is a program that receives inputs from agents with private preferences, and produces a public output. Rather than programming such a mechanism manually, the human designer writes a high-level partial specification that includes behavioral models of agents and a set of logical correctness requirements (for example, truth-telling) on the desired mechanism. A program synthesis algorithm is now used to automatically search a large space of candidate mechanisms and find one that satis es the requirements. The algorithm is based on a reduction to automated rst-order logic theorem proving | speci cally, deciding the satis ability of quanti er-free formulas in the rst-order theory of reals. We present an implementation of our synthesis approach on top of a Satis ability Modulo Theories solver. The system is evaluated through several case studies where we automatically synthesize a set of classic mechanisms and their variations, including the Vickrey auction, a multistage auction, a position auction, and a voting mechanism.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Vardi, Moshi (committee member), Nakhleh, Luay K. (committee member), Jermaine, Christopher M. (committee member).
Subjects/Keywords: program synthesis; economic mechanism design; game theory
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Fang, Y. (2015). computer-aided mechanism design. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/87798
Chicago Manual of Style (16th Edition):
Fang, Ye. “computer-aided mechanism design.” 2015. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/87798.
MLA Handbook (7th Edition):
Fang, Ye. “computer-aided mechanism design.” 2015. Web. 17 Jan 2021.
Vancouver:
Fang Y. computer-aided mechanism design. [Internet] [Masters thesis]. Rice University; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/87798.
Council of Science Editors:
Fang Y. computer-aided mechanism design. [Masters Thesis]. Rice University; 2015. Available from: http://hdl.handle.net/1911/87798
Rice University
17.
Imam, Shams Mahmood.
Cooperative Execution of Parallel Tasks with Synchronization Constraints.
Degree: PhD, Computer Science, 2015, Rice University
URL: http://hdl.handle.net/1911/88130
► The topic of this thesis is the effective execution of parallel applications on emerging multicore and manycore systems in the presence of modern synchronization and…
(more)
▼ The topic of this thesis is the effective execution of parallel applications on emerging multicore and manycore systems in the presence of modern synchronization and coordination constraints. Synchronization and coordination can contribute significant productivity and performance overheads to the development and execution of parallel programs. Higher-level programming models, such as the Task Parallel Model and Actor Model, provide abstractions that can be used to simplify writing parallel programs, in contrast to lower-level programming models that directly expose locks, threads and processes. However, these higher-level models often lack efficient support for general synchronization patterns that are necessary for a wide range of applications. Many modern synchronization and coordination constructs in parallel programs can incur significant performance overheads on current runtime systems, or significant productivity overheads when the programmer is forced to complicate their code to mitigate these performance overheads. We believe that a cooperation between the programmer and the runtime system is necessary to reduce the parallel overhead and to execute the available parallelism efficiently in the presence of synchronization constraints. In a cooperative approach, an executing entity yields control to other entities at well-defined points during its execution. This thesis shows that the use of cooperative techniques is critical to performance and scalability of certain parallel programming models, especially in the presence of modern synchronization and coordination constraints such as asynchronous tasks, futures, phasers, data-driven tasks, and actors. In particular, we focus on cooperative extensions and runtimes for the async-finish Task Parallel Model and the Actor Model in this thesis. Our work shows that cooperative techniques simplify programmability and deliver significant performance improvements by reducing the overhead in modern parallel programming models.
Advisors/Committee Members: Sarkat, Vivek (committee member), Mellor-Crummey, John (committee member), Chaudhuri, Swarat (committee member), Zhong, Lin (committee member).
Subjects/Keywords: Cooperative Techniques; Cooperative Runtime; Synchronization Constraints; Eureka Programming Model; Selector Model; Task Parallel Model; Actor Model; Habanero Java
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Imam, S. M. (2015). Cooperative Execution of Parallel Tasks with Synchronization Constraints. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/88130
Chicago Manual of Style (16th Edition):
Imam, Shams Mahmood. “Cooperative Execution of Parallel Tasks with Synchronization Constraints.” 2015. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88130.
MLA Handbook (7th Edition):
Imam, Shams Mahmood. “Cooperative Execution of Parallel Tasks with Synchronization Constraints.” 2015. Web. 17 Jan 2021.
Vancouver:
Imam SM. Cooperative Execution of Parallel Tasks with Synchronization Constraints. [Internet] [Doctoral dissertation]. Rice University; 2015. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88130.
Council of Science Editors:
Imam SM. Cooperative Execution of Parallel Tasks with Synchronization Constraints. [Doctoral Dissertation]. Rice University; 2015. Available from: http://hdl.handle.net/1911/88130
Rice University
18.
Prabhu, Sailesh Naveena.
A Constraint and Sampling-Based Approach to Integrated Task and Motion Planning.
Degree: MS, Engineering, 2014, Rice University
URL: http://hdl.handle.net/1911/88438
► This thesis tackles the Integrated Task and Motion Planning (ITMP) Problem. The ITMP problem extends classical task planning with actions that require a motion plan.…
(more)
▼ This thesis tackles the Integrated Task and Motion Planning (ITMP) Problem. The ITMP problem extends classical task planning with actions that require a motion plan. The agent seeks a sequence of actions and the necessary motions to achieve the goal.
The user partially specifies the task plan by providing the actions' known parameters. An SMT solver, then, discovers values for the unkown parameters that satisfies constraints requiring the task plan to achieve the goal. The SMT solver utilizes an annotated Probabilistic Roadmap (PRM) to query for motion planning information.
A sampling algorithm generates the PRM's vertices to permit a mobile manipulator to grasp numerous object configurations. Each iteration samples several base configurations and adds a base configuration to the PRM that increases the object configurations grasped from its vertices.
Our results indicate that increasing the samples per iteration improves the probability the SMT solver discovers a satisfying assignment without adversely affecting the resulting task plan.
Advisors/Committee Members: Chaudhuri, Swarat (advisor), Kavraki, Lydia E (committee member), McLurkin, James (committee member), Vardi, Moshe V (committee member).
Subjects/Keywords: Integrated Task and Motion Planning; planning from high-level specification; synthesis; constraint-based; sampling-based
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Prabhu, S. N. (2014). A Constraint and Sampling-Based Approach to Integrated Task and Motion Planning. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/88438
Chicago Manual of Style (16th Edition):
Prabhu, Sailesh Naveena. “A Constraint and Sampling-Based Approach to Integrated Task and Motion Planning.” 2014. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/88438.
MLA Handbook (7th Edition):
Prabhu, Sailesh Naveena. “A Constraint and Sampling-Based Approach to Integrated Task and Motion Planning.” 2014. Web. 17 Jan 2021.
Vancouver:
Prabhu SN. A Constraint and Sampling-Based Approach to Integrated Task and Motion Planning. [Internet] [Masters thesis]. Rice University; 2014. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/88438.
Council of Science Editors:
Prabhu SN. A Constraint and Sampling-Based Approach to Integrated Task and Motion Planning. [Masters Thesis]. Rice University; 2014. Available from: http://hdl.handle.net/1911/88438
Rice University
19.
Meel, Kuldeep Singh.
Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice.
Degree: PhD, Engineering, 2017, Rice University
URL: http://hdl.handle.net/1911/105480
► Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In constrained…
(more)
▼ Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In constrained counting, the task is to compute the total weight, subject to a given weighting function, of the set of solutions of the given constraints. In constrained sampling, the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. Consequently, Constrained counting and sampling have been subject to intense theoretical and empirical investigations over the years. Prior work, however, offered either heuristic techniques with poor guarantees of accuracy or approaches with proven guarantees but poor performance in practice.
In this thesis, we introduce a novel hashing-based algorithmic framework for constrained sampling and counting that combines the classical algorithmic technique of universal hashing with the dramatic progress made in Boolean reasoning solving, in particular, {\SAT} and {\SMT}, over the past two decades. By exploiting the connection between definability of formulas and variance of the distribution of solutions in a cell defined by 3-universal hash functions, we introduced an algorithmic technique, {\MIS}, that reduced the size of XOR constraints employed in the underlying universal hash functions by as much as two orders of magnitude. The resulting frameworks for counting ( {\ScalApproxMC}) and sampling ({\UniGen}) can handle formulas with up to million variables representing a significant boost up from the prior state of the art tools' capability to handle few hundreds of variables. If the initial set of constraints is expressed as Disjunctive Normal Form (DNF), {\ScalApproxMC} is the only known Fully Polynomial Randomized Approximation Scheme (FPRAS) that does not involve Monte Carlo steps.
We demonstrate the utility of the above techniques on various real applications including probabilistic inference, design verification and estimating the reliability of critical infrastructure networks during natural disasters. The high parallelizability of our approach opens up new directions for development of artificial intelligence tools that can effectively leverage high-performance computing resources.
Advisors/Committee Members: Chakraborty, Supratik (advisor), Chaudhuri, Swarat (committee member), Duenas-Osorio, Leonardo (committee member), Seshia, Sanjit A. (committee member), Vardi, Moshe Y. (committee member).
Subjects/Keywords: Constrained Counting; Constrained Sampling; SAT; universal hashing; SAT; SMT
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Meel, K. S. (2017). Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/105480
Chicago Manual of Style (16th Edition):
Meel, Kuldeep Singh. “Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice.” 2017. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/105480.
MLA Handbook (7th Edition):
Meel, Kuldeep Singh. “Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice.” 2017. Web. 17 Jan 2021.
Vancouver:
Meel KS. Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice. [Internet] [Doctoral dissertation]. Rice University; 2017. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/105480.
Council of Science Editors:
Meel KS. Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice. [Doctoral Dissertation]. Rice University; 2017. Available from: http://hdl.handle.net/1911/105480
20.
Imam, Shams.
Habanero-Scala: A Hybrid Programming model integrating Fork/Join and Actor models.
Degree: MS, Engineering, 2013, Rice University
URL: http://hdl.handle.net/1911/71662
► This study presents a hybrid concurrent programming model combining the previously developed Fork-Join model (FJM) and Actor model (AM). With the advent of multi-core computers,…
(more)
▼ This study presents a hybrid concurrent programming model combining the previously developed Fork-Join model (FJM) and Actor model (AM). With the advent of multi-core computers, there is a renewed interest in programming models that reduce the burden of reasoning about and writing efficient concurrent programs. The proposed hybrid model shows how the divide-and-conquer approach of the FJM and the no-shared mutable state and event-driven philosophy of the AM can be combined to solve certain classes of problems more efficiently and productively than either of the aforementioned models individually. The hybrid model adds actor creation and coordination
to into the FJM, while also enabling parallelization within actors. This study uses the Habanero-Java and Scala programming languages as the base for the FJM and AM respectively, and provides an implementation of the hybrid model as an extension of the Scala language called Habanero-Scala. The hybrid model adds to the foundations of parallel programs, and to the tools available for the programmer to aid in productivity and performance while developing parallel software.
Advisors/Committee Members: Sarkar, Vivek (advisor), Cartwright, Robert S. (committee member), Chaudhuri, Swarat (committee member).
Subjects/Keywords: Parallel programming; Actor model; Fork-join model; Async-finish model; Habanero-Scala
…Framework [23], OpenMP 3.0 [28] etc. At Rice University, we have
our own… …Habanero-C [30].
The Habanero Multicore Software Research Group at Rice University has… …Research Group at Rice University [29]. HJ supports AsyncFinish Model (AFM)…
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Imam, S. (2013). Habanero-Scala: A Hybrid Programming model integrating Fork/Join and Actor models. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/71662
Chicago Manual of Style (16th Edition):
Imam, Shams. “Habanero-Scala: A Hybrid Programming model integrating Fork/Join and Actor models.” 2013. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/71662.
MLA Handbook (7th Edition):
Imam, Shams. “Habanero-Scala: A Hybrid Programming model integrating Fork/Join and Actor models.” 2013. Web. 17 Jan 2021.
Vancouver:
Imam S. Habanero-Scala: A Hybrid Programming model integrating Fork/Join and Actor models. [Internet] [Masters thesis]. Rice University; 2013. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/71662.
Council of Science Editors:
Imam S. Habanero-Scala: A Hybrid Programming model integrating Fork/Join and Actor models. [Masters Thesis]. Rice University; 2013. Available from: http://hdl.handle.net/1911/71662
21.
Dutta, Sonali.
Assertion-Based Flow Monitoring of SystemC Models.
Degree: MS, Engineering, 2014, Rice University
URL: http://hdl.handle.net/1911/76706
► SystemC is the de facto system modeling language, and verification of SystemC models is a major research direction. Assertion-Based Monitoring is a dynamic verification technique…
(more)
▼ SystemC is the de facto system modeling language, and verification of SystemC models is a major research direction. Assertion-Based Monitoring is a dynamic verification technique that allows the user to dynamically verify formal properties of the system by automatically generating runtime monitors from them.
A typical hardware-software system is concurrent and reactive. Examples of such systems can be a computer, an ATM server etc. Such systems perform multiple jobs of different types during their execution. For example, different types of jobs in a computer can be ‘launching a web browser’, ‘searching the file system’ etc. A job can be submitted by an external user or generated by an internal component of the system. A job can begin at any point in time during the execution of the system, the beginning time being completely unknown beforehand. A job begins with a set of inputs, travels from one system component to another to generate a set of outputs and ends after a finite amount of time. Since a job “flows” among the system components, we call it a flow. In a concurrent system multiple flows can begin and travel though the system at the same time. This work focuses on verifying formal properties about these dynamic and concurrent flows (called flow properties) in a concurrent reactive system, modeled in SystemC.
The contribution of this thesis is three fold: First, a light-weight C++ library, called
iii
Flow Library, that enables modeling of flows in SystemC in a structured manner. Second, an algorithm, implemented in the FlowMonGen tool, to generate C++ monitor class from a flow property, which is an LTL formula interpreted over the finite trace of a flow. Third, a dynamic and decentralized algorithm to monitor the concurrent flows in a SystemC model. Our completely automated and efficient Flow Monitoring Framework implements this algorithm.
Advisors/Committee Members: Vardi, Moshe Y. (advisor), Chaudhuri, Swarat (committee member), Nakhleh, Luay K. (committee member).
Subjects/Keywords: Flow-monitoring; SystemC; Assertion; Monitor; Flow property; Flow type; Flow attribute; Dynamic; Decentralized; Concurrent; Alive; Flow
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Dutta, S. (2014). Assertion-Based Flow Monitoring of SystemC Models. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/76706
Chicago Manual of Style (16th Edition):
Dutta, Sonali. “Assertion-Based Flow Monitoring of SystemC Models.” 2014. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/76706.
MLA Handbook (7th Edition):
Dutta, Sonali. “Assertion-Based Flow Monitoring of SystemC Models.” 2014. Web. 17 Jan 2021.
Vancouver:
Dutta S. Assertion-Based Flow Monitoring of SystemC Models. [Internet] [Masters thesis]. Rice University; 2014. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/76706.
Council of Science Editors:
Dutta S. Assertion-Based Flow Monitoring of SystemC Models. [Masters Thesis]. Rice University; 2014. Available from: http://hdl.handle.net/1911/76706
22.
Drummond, Anna.
Statistical Machine Learning for Text Mining with Markov Chain Monte Carlo Inference.
Degree: PhD, Engineering, 2014, Rice University
URL: http://hdl.handle.net/1911/76711
► This work concentrates on mining textual data. In particular, I apply Statistical Machine Learning to document clustering, predictive modeling, and document classification tasks undertaken in…
(more)
▼ This work concentrates on mining textual data. In particular, I apply Statistical Machine Learning to document clustering, predictive modeling, and document classification tasks undertaken in three different application domains. I have designed novel statistical Bayesian models for each application domain, as well as derived Markov Chain Monte Carlo (MCMC) algorithms for the model inference.
First, I investigate the usefulness of using topic models, such as the popular Latent Dirichlet Allocation (LDA) and its extensions, as a pre-processing feature selection step for unsupervised document clustering. Documents are clustered using the pro- portion of the various topics that are present in each document; the topic proportion vectors are then used as an input to an unsupervised clustering algorithm. I analyze two approaches to topic model design utilized in the pre-processing step: (1) A traditional topic model, such as LDA (2) A novel topic model integrating a discrete mixture to simultaneously learn the clustering structure and the topic model that is conducive to the learned structure. I propose two variants of the second approach, one of which is experimentally found to be the best option. Given that clustering is one of the most common data mining tasks, it seems like an obvious application for topic modeling.
Second, I focus on automatically evaluating the quality of programming assignments produced by students in a Massive Open Online Course (MOOC), specifically an interactive game programming course, where automated test-based grading is not applicable due the the character of the assignments (i.e., interactive computer games). Automatically evaluating interactive computer games is not easy because such pro- grams lack any sort of well-defined logical specification, so it is difficult to devise a testing platform that can play a student-coded game to determine whether it is correct. I propose a stochastic model that given a set of user-defined metrics and graded example programs, can learn, without running the programs and without a grading rubric, to assign scores that are predictive of what a human (i.e., peer-grader) would give to ungraded assignments.
The main goal of the third problem I consider is email/document classification. I concentrate on incorporating the information about senders/receivers/authors of a document to solve a supervised classification problem. I propose a novel vectorized representation for people associated with a document. People are placed in the latent space of a chosen dimensionality and have a set of weights specific to the roles they can play (e.g., in the email case, the categories would be TO, FROM, CC, and BCC). The latent space positions together with the weights are used to map a set of people to a vector by taking a weighted average. In particular, a multi-labeled email classification problem is considered, where an email can be relevant to all/some/none of the desired categories. I develop three stochastic models that can be used to learn to predict multiple labels,…
Advisors/Committee Members: Jermaine, Christopher M. (advisor), Nakhleh, Luay K. (committee member), Chaudhuri, Swarat (committee member), Allen, Genevera (committee member).
Subjects/Keywords: Bayesian modeling; Text mining; Machine learning; MCMC
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Drummond, A. (2014). Statistical Machine Learning for Text Mining with Markov Chain Monte Carlo Inference. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/76711
Chicago Manual of Style (16th Edition):
Drummond, Anna. “Statistical Machine Learning for Text Mining with Markov Chain Monte Carlo Inference.” 2014. Doctoral Dissertation, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/76711.
MLA Handbook (7th Edition):
Drummond, Anna. “Statistical Machine Learning for Text Mining with Markov Chain Monte Carlo Inference.” 2014. Web. 17 Jan 2021.
Vancouver:
Drummond A. Statistical Machine Learning for Text Mining with Markov Chain Monte Carlo Inference. [Internet] [Doctoral dissertation]. Rice University; 2014. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/76711.
Council of Science Editors:
Drummond A. Statistical Machine Learning for Text Mining with Markov Chain Monte Carlo Inference. [Doctoral Dissertation]. Rice University; 2014. Available from: http://hdl.handle.net/1911/76711
23.
Meel, Kuldeep.
Sampling Techniques for Boolean Satisfiability.
Degree: MS, Engineering, 2014, Rice University
URL: http://hdl.handle.net/1911/77222
► Boolean satisfiability (SAT) has played a key role in diverse areas spanning testing, formal verification, planning, optimization, inferencing and the like. Apart from the classical…
(more)
▼ Boolean satisfiability (SAT) has played a key role in diverse areas spanning testing, formal verification,
planning, optimization, inferencing and the like. Apart from the classical problem of checking boolean satisfiability, the problems of generating satisfying uniformly at random, and of counting the total number of satisfying assignments have also attracted significant theoretical and practical interest over the years. Prior work offered
heuristic approaches with very weak or no guarantee of performance, and theoretical
approaches with proven guarantees, but poor performance in
practice.
We propose a novel approach based on limited-independence hashing that allows us to design algorithms for both problems, with strong theoretical guarantees and scalability extending to thousands of variables. Based on this approach, we present two practical algorithms, UniWit: a near uniform generator and ApproxMC: the first scalable approximate model counter, along with reference implementations. Our algorithms work by issuing polynomial calls to SAT solver. We demonstrate scalability of our algorithms over a large set of benchmarks arising from different application domains.
Advisors/Committee Members: Vardi, Moshe Y. (advisor), Chakraborty, Supratik (committee member), Chaudhuri, Swarat (committee member), Nakhleh, Luay K. (committee member).
Subjects/Keywords: SAT; Uniform generation; Model counting; Sampling techniques; Computer aided verification
Record Details
Similar Records
Cite
Share »
Record Details
Similar Records
Cite
« Share
❌
APA ·
Chicago ·
MLA ·
Vancouver ·
CSE |
Export
to Zotero / EndNote / Reference
Manager
APA (6th Edition):
Meel, K. (2014). Sampling Techniques for Boolean Satisfiability. (Masters Thesis). Rice University. Retrieved from http://hdl.handle.net/1911/77222
Chicago Manual of Style (16th Edition):
Meel, Kuldeep. “Sampling Techniques for Boolean Satisfiability.” 2014. Masters Thesis, Rice University. Accessed January 17, 2021.
http://hdl.handle.net/1911/77222.
MLA Handbook (7th Edition):
Meel, Kuldeep. “Sampling Techniques for Boolean Satisfiability.” 2014. Web. 17 Jan 2021.
Vancouver:
Meel K. Sampling Techniques for Boolean Satisfiability. [Internet] [Masters thesis]. Rice University; 2014. [cited 2021 Jan 17].
Available from: http://hdl.handle.net/1911/77222.
Council of Science Editors:
Meel K. Sampling Techniques for Boolean Satisfiability. [Masters Thesis]. Rice University; 2014. Available from: http://hdl.handle.net/1911/77222
. 
Open Access Theses and Dissertations
