Tesi honek FTL-CFree zehazteko lengoaia aurkezten du. Hark semantika zirriborrotsua eta aldagaiak zenbakiz adierazteko ahalmena gehitzen dizkio denbora-logikari, lerroan egiaztatzeko eremuan aplikatzeko. Lengoaiaren semantika bilakatzen da zirriborrotsuki, zeren eta sarrera aztarna bat interpretatzeak baieztapen baten ziurtasuna adierazteaz gain, nola ezaugarria bilakatuko den ere azaltzen baitu, atzizki gehiago aztarnari erantziz gero. Lerroan egiaztatzean ohikoa denez, lengoaiak orakulu egokia sortzen du; hortaz, zehaztapen behagarri bat lortu ahal da, sistema baten goi-mailako betekizunetatik. Lerroan egiaztatzeak sistema bati buruzko informazioa ematen du uneoro. Halaber, ingeniariei oso lagungarri zaie egoera analizatzeko ahalmena, ikuspegi geldikor batetik, sistemak baldintza izendatuetan jokatzen duenean. FTL-CFree lengoaiak deskribaturiko zehaztapenaren betekizun bat ebaluatzeari eragiten dio sistemaren beraren barne-aldaketak; horregatik, haren erantzunaren ezaugarriak estatistikoki adieraztea gogoko dugu biziki. FTL-CFree-aren semantikak neurri zirriborrotsu bihurtzen du sarrera testuinguru bat, horrela ausazko aldagai gisa analiza daiteke. Bide horretan frogatzen da FTL-CFree formula batek probabilitate banaketa jakin bati jarraitzen diola eta baieztatzen da, zirriborrotsuki neurtzean, ausazko ziurgabetasunaren ezaugarriak deskribatu ahal dituela probabilitate teoriak. FTL-CFree ausazko aldagaia abiapuntu hartuz, eta probabilitatea baldintza izendatuetara mugatuz, formulak parametroen bidez adierazteko metodo bat garatu da.