Research Topics

This project is a multi-disciplinary research project that involves computer science theory, programming, engineering design, operation test, fluid dynamics, kenematics analysis, VLSI design, stress test, etc.

We have a team of engineering students that are enthusathimic, highly motivated and skillful, collaborative on the cutting edge research of multiple drone design and artificial intelligence applications.

Key Research Topics

Formal Methods & Temporal Logic

[Wiki] In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

[Standford Encyclopedia] The term Temporal Logic has been broadly used to cover all approaches to reasoning about time and temporal information, as well as their formal representation, within a logical framework, and also more narrowly to refer specifically to the modal-logic type of approach

Model Checking

[CMU] Model checking is a method for formally verifying finite-state concurrent systems. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. Extremely large state-spaces can often be traversed in minutes. The technique has been applied to several complex industrial systems such as the Futurebus+ and the PCI local bus protocols.

Python Programming

Python is a programming language that lets you work quicklyand integrate systems more effectively. Experienced programmers in any other language can pick up Python very quickly, and beginners find the clean syntax and indentation structure easy to learn.

Many tutorials are available for Python. The official document and software are available at https://www.python.org/. A free Python tutorial can be found at YouTube https://www.youtube.com/watch?v=eWRfhZUzrAc. Sololearn has the playground for Python https://www.sololearn.com/.

Deep Learning & Reinforcement Learning

Deep Learning (DL) and Reinforcement Learning (RL) are the subfields of the machine learning which is a subarea of artificial intelligence. [Wiki] DL is a form of machine learning that utilizes a neural network to transform a set of inputs into a set of outputs via an artificial neural network. Deep learning methods, often using supervised learning with labeled datasets, have been shown to solve tasks that involve handling complex, high-dimensional raw input data such as images, with less manual feature engineering. RL is a process in which an agent learns to make decisions through trial and error.. A tutorial can be found at Mathworks https://www.mathworks.com/.

Quadcopter Dynamics, Control and Simulation

A quadrotor helicopter (quadcopter) is a helicopter which has four equally spaced rotors, usually arranged at the corners of a square body. With four independent rotors, the need for a swashplate mechanism is alleviated. The swashplate mechanism was needed to allow the helicopter to utilize more degrees of freedom, but the same level of control can be obtained by adding two more rotors.

Quadcopter control is a fundamentally difficult and interesting problem. With six degrees of freedom (three translational and three rotational) and only four independent inputs (rotor speeds), quadcopters are severely underactuated. In order to achieve six degrees of freedom, rotational and translational motion are coupled. The resulting dynamics are highly nonlinear, especially after accounting for the complicated aerodynamic effects. Finally, unlike ground vehicles, helicopters have very little friction to prevent their motion, so they must provide their own damping in order to stop moving and remain stable. Together, these factors create a very interesting control problem.

Control Synthesis

To synthesize a control policy and maximize probability
that an LTL specification is satisfied in unknown stochastic environments, we adopt a framework of MDP reinforcement learning model of the environment. Starting from synthsizing an LTL specification on the MDP is to synthesize a policy of a B¨uchi objective on the product MDP. We need to design a reward scheme, and show that the memoryless policy optimizing this reward, also optimizes the satisfaction probability of the B¨uchi objective (and thus the initial LTL specification).