Monitorabilidade Relativa à Observação da Implicação Temporal Limitada

Um condicional material "P implica Q" possui um valor de verdade atemporal, mas saber se ele é verdadeiro não possui: cada verificação física ou computacional do condicional é um ato de observação, realizado com resolução finita, com cada evento separado de sua observação por atraso, deriva e jitter. Isso produz um paradoxo de implicação observada -- um monitor internamente sólido pode contradizer o valor de verdade atemporal em ambas as direções (um falso contrafactual, ou um disparador fantasma), não porque o instrumento está quebrado, mas porque a observação possui uma classe. Tornamos isso preciso para a implicação temporal G(p -> F<=k q) e estabelecemos um único resultado principal: a monitorabilidade da implicação limitada é conjunta no par (fórmula, modelo de observação) -- o modelo de observação sendo o regime de amostragem através do qual os sinais são lidos (quando o monitor observa, e o atraso, deriva, jitter e resolução finita entre um evento e sua observação) -- e não é uma propriedade apenas da fórmula. Uma mudança apenas no modelo de observação pode mover a propriedade pela classificação de segurança / cossegurança / vivacidade / colivacidade. O espaço de observação se divide em uma taxonomia verificada por máquina de oito classes; uma escada monotônica de teorias de observação declara quais classes se tornam atribuíveis como verdadeiras; e observadores internamente sólidos que discordam ocupam degraus diferentes ao invés de se contradizerem. Pré-impressão; uma versão foi preparada para submissão. Companheiro de engenharia: "Controlando a Classe de Observação de um Monitor em Tempo de Execução" (co-depositado).