  We study the problem of synthesizing a controller to satisfy a complex task
in the presence of sensor faults and attacks. We model the task using Gaussian
distribution temporal logic (GDTL), and propose a solution approach that does
not rely on computing any finite abstraction to model the system. We decompose
the GDTL specification into a sequence of reach-avoid sub-tasks. We develop a
class of fault-tolerant finite time convergence control barrier functions
(CBFs) to guarantee that a dynamical system reaches a set within finite time
almost surely in the presence of malicious attacks. We use the fault-tolerant
finite time convergence CBFs to guarantee the satisfaction of `reach' property.
We ensure `avoid' part in each sub-task using fault-tolerant zeroing CBFs.
These fault-tolerant CBFs formulate a set of linear constraints on the control
input for each sub-task. We prove that if the error incurred by system state
estimation is bounded by a certain threshold, then our synthesized controller
fulfills each reach-avoid sub-task almost surely for any possible sensor fault
and attack, and thus the GDTL specification is satisfied with probability one.
We demonstrate our proposed approach using a numerical study on the
coordination of two wheeled mobile robots.
