Skip to content

Case StudiesΒΆ

In the following sections we will present case studies that illustrate the use of Pacti for different applications.

We present a case study to evaluate the perception system of an autonomous car using the quotient operator.

multiagent figure

A case study on multi-agent path finding (MAPF) where multiple agents need to reach their target location on a grid world according to a conflict-free strategy. We treat each time step as our viewpoint to find a solution that satisfies the agents' dynamics and collision constraints using the merge operator.

multiagent figure

A case study on modeling the specifications of a biological circuit and speed up the experimental design process by finding optimal components to use from a library of parts. In the case study, we first build a characterized library of parts as assume-guarantee contracts using existing experimental data from the literature.With the use of Pacti, we demonstrate how scientists may describe the desired top-level behavior as contracts and then computationally choose from a library of available parts to ensure that the components meet the top-level system specification. For the engineered bacteria case study, we find the specification of the sensors that meet the top-level criteria on fold-change of the circuit response. Finally, we also show how we can find the specifications of missing parts in a system. In synthetic biology, it is common to have parts in the system for which no characterization data is available. Using quotient operation on contracts, we can find the constraints that this missing part must satisfy to meet the desired top-level criteria.

Biocircuit Specifications Case Study Overview

A case study on word length analysis and optimization for digital signal processing circuit design.

DSP figure

We demonstrate the application of Pacti in modeling a context-sensitive grammar for generating three-dimensional topologies for Unmanned Aerial Vehicles (UAVs).

uav topologies

A case study on modeling the specifications of autonomous tasks for a planning/scheduling onboard of a space mission system.

Space Mission Autonomy

A case study on modeling a simplified timeline of the Mars 2020 Entry-Descent-Landing.

Mars EDL