மாதிரிகளும் சரிபார்ப்பும்
***********************************
மாதிரி (Model) சரிபார்ப்பு (Checking) என்பது  ஒரு வன்பொருள்(Hardware) அல்லது
மென்பொருள் (Software) அமைவின் (System)  மாதிரியானது, தனக்குப் பொருந்தக்கூடிய
நிலையற்ற (Temporal) தருக்க (Logic) சுருக்கவிதிமுறை( Formula) களால்
குறிப்பிடப்பட்ட முறைசார்ந்த (Formal) அதன் குறியீடுகளை (Specification)
நிறை (Satisfy) செய்கிறதா அல்லது  இல்லையா என சரிபார்ப்பதே ஆகும்.

அந்த சுருக்க விதிமுறைகளானது ,
ஒருமுக நேர்காலத் தருக்கமாகவோ (Linear Time Logic)  அல்லது
பன்முக கணனிபடர் தருக்கமாகவோ (Computational Tree Logic) அமையப் பெறலாம்.

இது போன்ற மாதிரிகள், உருபெறப் போகும் ஒரு அமைவின் இயங்குநிலை நடத்தைகளை  அகப்படுத்தி வெளிப்படுத்தும் அமைப்பு ஆகும்.
பொதுவாக இவற்றை " க்ரிப்கே"( Kripke)  உருஅமைப்பு( Structure) எனச் சொல்வார்கள்.

ஒருமுக நேர்காலத் தருக்கம் (Linear Time Logic) :
***************************************************************
இந்த வழியைப் பின்பற்றி வரும் சுருக்கவிதிமுறை (Formulas) களை  

       "ஒ"   எனக் கொள்வோமேயானால்,
அந்த "ஒ" விதிமுறைகளை ஏற்பு இல்லா மறுப்பு (Non-Negated) படிவம் (Form) தாங்கி
பின்வருமாறு வெளிப்படையாகத் தெரிவிக்கலாம் .

            "ஒ" = உண்மை ( true) | பொய் (false) | எனவும்
              அடிப்படைக்கூற்று (proposition) கூ | எனவும்
மறுக்கப்பட்ட கூற்று (negated proposition) ம கூ | குறிக்கப்படலாம்.

இரு வெவ்வேறு விதிமுறைகளின் குறுக்கீட்டுச் சந்திப்பு (Intersection of two different formulas) :                கூ1 குறுக்கு கூ2     ஆகியவையாகவோ, மேலும்

          "ஒ" = அடுத்த (Next) எனும் வினைக்குறி (Operator) |
                 = இறுதியாக (Eventually) எனும் வினைக்குறி
                 = எப்போதும் (Always)எனும் வினைக்குறி |

                 = வரையிலும் ( Until) எனும் வினைக்குறி |
                  = கட்டவிழ்ப்பு ( Release )எனும் வினைக்குறி
                   = நலிந்த வரையிலும் ( Weak Until) எனும் வினைக்குறி
என்பனவற்றை,

அ"ஒ" | இ"ஒ" | எ"ஒ" | வ"ஒ" | க "ஒ" | ந "ஒ"      எனவும்  குறிப்பிட இயலும்..